Skip to content

Non working example in the documentation

ID0001098: This issue was created automatically from Mantis Issue 1098. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001098 Frama-C Documentation public 2012-02-17 2016-08-31
Reporter ploc Assigned To virgile Resolution fixed
Priority normal Severity minor Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version Frama-C Sodium Fixed in Version Frama-C Sodium

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information