Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001098Frama-CDocumentationpublic2012-02-17 22:462016-08-31 19:34
Reporterploc 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFrama-C SodiumFixed in VersionFrama-C Sodium 
Summary0001098: Non working example in the documentation
DescriptionIn 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002709)
ploc (reporter)
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 (reporter)
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 (developer)
2015-02-03 15:25

 Fix committed to master branch.
(0006258)
signoles (manager)
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.

- Issue History
Date Modified Username Field Change
2012-02-17 22:46 ploc New Issue
2012-02-17 22:46 ploc Status new => assigned
2012-02-17 22:46 ploc Assigned To => signoles
2012-02-17 22:51 ploc Note Added: 0002709
2012-02-28 13:50 monate Note Added: 0002741
2012-02-28 13:51 monate Assigned To signoles => monate
2012-02-28 13:51 monate Status assigned => confirmed
2015-01-19 17:40 signoles Assigned To monate => virgile
2015-01-19 17:40 signoles Status confirmed => assigned
2015-01-19 17:40 signoles Status assigned => confirmed
2015-01-26 11:23 signoles Target Version => Frama-C Sodium
2015-02-03 15:25 virgile Note Added: 0005683
2015-02-03 15:25 virgile Status confirmed => resolved
2015-02-03 15:25 virgile Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:16 signoles Category Documentation > ACSL => Documentation
2016-08-31 19:34 signoles Note Added: 0006258

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker