Frama-C Bug Tracking System - Frama-C
View Issue Details
0001098Frama-CDocumentationpublic2012-02-17 22:462016-08-31 19:34
ploc 
virgile 
normalminorhave not tried
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C SodiumFrama-C Sodium 
0001098: Non working example in the documentation
In logic_typing.ml the example to illustrate the definition of a new keyword is not typable. The correct version is : let foo_typer ~typing_context ~loc bhv ps = match ps with | p::[] -> bhv.b_extended <- ("FOO",42, [Logic_const.new_predicate (typing_context.type_predicate (typing_context.post_state [Normal]) p)]) ::bhv.b_extended | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = register_behavior_extension "FOO" foo_typer
No tags attached.
Issue History
2012-02-17 22:46plocNew Issue
2012-02-17 22:46plocStatusnew => assigned
2012-02-17 22:46plocAssigned To => signoles
2012-02-17 22:51plocNote Added: 0002709
2012-02-28 13:50monateNote Added: 0002741
2012-02-28 13:51monateAssigned Tosignoles => monate
2012-02-28 13:51monateStatusassigned => confirmed
2015-01-19 17:40signolesAssigned Tomonate => virgile
2015-01-19 17:40signolesStatusconfirmed => assigned
2015-01-19 17:40signolesStatusassigned => confirmed
2015-01-26 11:23signolesTarget Version => Frama-C Sodium
2015-02-03 15:25virgileNote Added: 0005683
2015-02-03 15:25virgileStatusconfirmed => resolved
2015-02-03 15:25virgileResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:18signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:16signolesCategoryDocumentation > ACSL => Documentation
2016-08-31 19:34signolesNote Added: 0006258

Notes
(0002709)
ploc   
2012-02-17 22:51   
As a general remark the syntax extension is really not well documented. I parsed all the mailing list without any good elements. Then I had to precisely look into the source to understand it. However, the use of the type mutable b_extended : (string * int * 'a list) list; (* Grammar extensions *) in Behaviors is still not documented. What is the int and what is the meaning/use of the 'a list, the list of the arguments ? If so, you should write it somewhere.
(0002741)
monate   
2012-02-28 13:50   
You are right: the syntax extension mechanism is completly undocumented. The main reason is that we have not yet frozen the API for these extensions. As soon as something satisfactory will be available, it will be documented but do not hold your breath. If you have specific industrial level needs we can speed up this process thanks to a commercial support contract. I'll leave the report open as a feature request.
(0005683)
virgile   
2015-02-03 15:25   
Fix committed to master branch.
(0006258)
signoles   
2016-08-31 19:34   
A new section documenting the syntax extension mechanism has been added in the Plug-in Development Guide. It will be part of the next public release (Frama-C Silicium). BTW the mechanism has been improved but the interface has changed: the client code must be migrated. It should be rather easy thanks to the new documentation.