| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001098 | Frama-C | Documentation | public | 2012-02-17 22:46 | 2016-08-31 19:34 | ||||
| Reporter | ploc | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Frama-C Sodium | Fixed in Version | Frama-C Sodium | ||||||
| Summary | 0001098: Non working example in the documentation | ||||||||
| Description | 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
|
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. |
|
virgile (developer) 2015-02-03 15:25 |
Fix committed to master branch. |
|
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. |
| Notes |
| 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 | Source_changeset_attached | => framac master e5b49198 |
| 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 | |
| Issue History |