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