Merge pull request #1057 from dewert99/simple-trigger-specs

Fix bug in creation of spec axioms

creusot/src/backend/logic.rs

@@ -185,9 +185,9 @@ pub(crate) fn lower_logical_defn<'tcx, N: Namer<'tcx>>(
     );
 
     if has_axioms {
-        if sig.uses_simple_triggers() {
+        if sig.uses_simple_triggers() && !sig_contract.contract.variant.is_empty() {
             let lim_name = Ident::from_string(format!("{}_lim", &*sig.name));
-            let mut lim_sig = sig.clone();
+            let mut lim_sig = sig_contract;
             lim_sig.name = lim_name;
             lim_sig.trigger = Some(Trigger::single(function_call(&lim_sig)));
             lim_sig.attrs = vec![];

creusot/tests/should_succeed/simple_trigger.coma

@@ -0,0 +1,52 @@
+
+module SimpleTrigger_Id_Impl
+  let%span ssimple_trigger0 = "../simple_trigger.rs" 7 11 7 17
+
+  let%span ssimple_trigger1 = "../simple_trigger.rs" 9 0 9 34
+
+  let%span ssimple_trigger2 = "../simple_trigger.rs" 8 10 8 11
+
+  use prelude.prelude.Int
+
+  constant i  : int
+
+  function id [#"../simple_trigger.rs" 10 0 10 20] (i : int) : int
+
+  goal vc_id : ([%#ssimple_trigger0] i >= 0)
+   -> (if i = 0 then
+    [%#ssimple_trigger1] i = 0  -> 0 = 0
+  else
+    (([%#ssimple_trigger0] i - 1 >= 0)
+    /\ 0 <= ([%#ssimple_trigger2] i) /\ ([%#ssimple_trigger2] i - 1) < ([%#ssimple_trigger2] i))
+    /\ (([%#ssimple_trigger1] i - 1 = 0  -> id (i - 1) = 0)  -> ([%#ssimple_trigger1] i = 0  -> id (i - 1) + 1 = 0))
+  )
+end
+module SimpleTrigger_Test
+  let%span ssimple_trigger0 = "../simple_trigger.rs" 18 10 18 20
+
+  let%span span1 = "../simple_trigger.rs" 7 11 7 17
+
+  let%span span2 = "../simple_trigger.rs" 9 0 9 34
+
+  let%span span3 = "../simple_trigger.rs" 8 10 8 11
+
+  let%span span4 = "../simple_trigger.rs" 6 0 6 8
+
+  use prelude.prelude.Int
+
+  function id'0 [#"../simple_trigger.rs" 10 0 10 20] (i : int) : int
+
+  function id'0_lim (i : int) : int
+
+  axiom id'0_def : forall i : int [id'0 i] . id'0 i = ([%#span4] if i = 0 then 0 else id'0_lim (i - 1) + 1)
+
+  axiom id'0_def_lim : forall i : int [id'0 i] . id'0 i = id'0_lim i
+
+  axiom id'0_lim_spec : forall i : int [id'0_lim i] . ([%#span1] i >= 0)  -> ([%#span2] i = 0  -> id'0_lim i = 0)
+
+  use prelude.prelude.Intrinsic
+
+  let rec test (_1:()) (return'  (ret:()))= (! bb0 [ bb0 = return' {_0} ] ) [ & _0 : () = any_l () ] 
+    [ return' (result:())-> {[@expl:postcondition] [%#ssimple_trigger0] id'0 1 = 1} (! return' {result}) ]
+
+end

creusot/tests/should_succeed/simple_trigger.rs

@@ -0,0 +1,19 @@
+// CREUSOT_ARG=--simple-triggers=true
+extern crate creusot_contracts;
+
+use creusot_contracts::*;
+
+#[logic]
+#[requires(i >= 0)]
+#[variant(i)]
+#[ensures(i == 0 ==> result == 0)]
+fn id(i: Int) -> Int {
+    if i == 0 {
+        0
+    } else {
+        id(i - 1) + 1
+    }
+}
+
+#[ensures(id(1) == 1)]
+pub fn test() {}

creusot/tests/should_succeed/simple_trigger/why3session.xml

@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"https://www.why3.org/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="Z3" version="4.12.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<file format="coma" proved="true">
+<path name=".."/><path name="simple_trigger.coma"/>
+<theory name="SimpleTrigger_Id_Impl" proved="true">
+ <goal name="vc_id" proved="true">
+ <proof prover="0"><result status="valid" time="0.031265" steps="314"/></proof>
+ </goal>
+</theory>
+<theory name="SimpleTrigger_Test" proved="true">
+ <goal name="vc_test" proved="true">
+ <proof prover="0"><result status="valid" time="0.024485" steps="1167"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>