Skip to content
Snippets Groups Projects
Commit 282c5387 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[devman] fixes example of ACSL extension (and Makefile `check` rule :disappointed:)

parent 3518e275
No related branches found
No related tags found
No related merge requests found
...@@ -49,7 +49,7 @@ else ...@@ -49,7 +49,7 @@ else
-load-script ./examples/acsl_extension \ -load-script ./examples/acsl_extension \
-load-script ./hello_world/hello_world.ml \ -load-script ./hello_world/hello_world.ml \
| tee check.log | tee check.log
if grep -e "user error" check.log; then \ if grep -e "User Error" check.log; then \
echo "Examples script do not compile with current Frama-C."; \ echo "Examples script do not compile with current Frama-C."; \
echo "Please examine check.log and make appropriate changes"; \ echo "Please examine check.log and make appropriate changes"; \
exit 1; \ exit 1; \
......
...@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l = ...@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l =
in in
Ext_terms res Ext_terms res
let () = Logic_typing.register_behavior_extension "foo" type_foo let () = Logic_typing.register_behavior_extension "foo" false type_foo
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment