Print warning recommending contract assumptions over assertions

daniel-larraz · Oct 30, 2023 · c53aba0 · c53aba0
1 parent 47d2dfb
commit c53aba0
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml
@@ -83,9 +83,12 @@ type error = [
 
 type warning_kind = 
   | UnguardedPreWarning of A.expr
+  | UseOfAssertionWarning
 
 let warning_message warning = match warning with
   | UnguardedPreWarning expr -> "Unguarded pre in expression " ^ A.string_of_expr expr
+  | UseOfAssertionWarning ->
+    "Assertions are not checked; please consider using a contract assumption instead"
 
 type warning = [
   | `LustreAstNormalizerWarning of Lib.position * warning_kind
@@ -1047,6 +1050,7 @@ and normalize_contract info map items =
 and normalize_equation info map = function
   | Assert (pos, expr) ->
     let nexpr, map, warnings = abstract_expr true info map true expr in
+    let warnings = mk_warning pos UseOfAssertionWarning :: warnings in
     A.Assert (pos, nexpr), map, warnings
   | Equation (pos, lhs, expr) ->
     (* Need to track array indexes of the left hand side if there are any *)

diff --git a/src/lustre/lustreAstNormalizer.mli b/src/lustre/lustreAstNormalizer.mli
@@ -72,6 +72,7 @@ type error = [
 
 type warning_kind =
   | UnguardedPreWarning of LustreAst.expr
+  | UseOfAssertionWarning
 
 type warning = [
   | `LustreAstNormalizerWarning of Lib.position * warning_kind