Modifies proofs partially working

At the moment, if there is a specification and DONT_TRANSLATE, the
automatic proofs only work if the specification is that no globals are
modified.

Work on JIRA VER-464

tools/c-parser/HPInter.ML

@@ -259,12 +259,19 @@ fun mkSpecFunction thy gloc cse styargs (f : fninfo) = let
   val mod_spec = collect_t $ list_mk_pabs([s,t], relbody)
   val _ = Feedback.informStr(0, "modstr : " ^ typedterm mod_spec)
   val otherspecs = List.concat (map (parse_spec thy) (#spec f))
-  val _ = appi (fn n => fn t => Feedback.informStr(0,
-    "spec#" ^ Int.toString n ^ ": " ^ typedterm t)) otherspecs
-  val spec_t = List.foldl mk_inter mod_spec otherspecs
-  val fbody = Const(@{const_name "guarded_spec_body"},
+  val fbody =
+    if null otherspecs then
+      mk_Spec(styargs, mod_spec)
+    else
+      let
+        val _ = appi (fn n => fn t => Feedback.informStr(0,
+                       "spec#" ^ Int.toString n ^ ": " ^ typedterm t)) otherspecs
+        val spec_t = List.foldl mk_inter mod_spec otherspecs
+      in
+        Const(@{const_name "guarded_spec_body"},
                     @{typ "strictc_errortype"} --> type_of spec_t -->
                     mk_com_ty styargs) $ @{const "ImpossibleSpec"}  $ spec_t
+      end
 in
   (fname, fbody, fbody)
 end

tools/c-parser/modifies_proofs.ML

@@ -224,23 +224,8 @@ fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let
                         NONE => Binaryset.empty String.compare
                       | SOME s => s
           val i = Binaryset.intersection(calls, failedsofar)
-          fun fnspec s = case s of Absyn.fnspec _ => true | _ => false
-          val has_definition =
-              isSome (Symtab.lookup (get_defined_functions csenv) fname)
-          val has_fnspec =
-            case Symtab.lookup (function_specs csenv) fname of
-              NONE => false
-            | SOME l => List.exists fnspec l
-          (* even if there is no body; try to do a modifies proof in the
-             absence of specs as it is these that really confuse things.
-
-             You can write DONT_TRANSLATE on top of a function and provide just
-             a MODIFIES clause, and modifies proofs in these situations work.
-             This scenario may not be likely
-          *)
-          val translated = has_definition orelse not has_fnspec
         in
-          if Binaryset.isEmpty i andalso translated then let
+          if Binaryset.isEmpty i then let
               val thy = Proof_Context.theory_of lthy
               val goal = gen_modify_goal thy tyargs gamma_t fname mvlist
               fun tac ctxt = let
@@ -258,7 +243,7 @@ fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let
             in
               (failedsofar, lthy) before modifies_msg "successful"
             end
-          else if translated then let
+          else let
               val example = valOf (Binaryset.find (fn _ => true) i)
               val _ = modifies_msg
                           ("not attempted, as it calls a function ("
@@ -266,10 +251,6 @@ fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let
             in
               (Binaryset.add(failedsofar, fname), lthy)
             end
-          else
-            (modifies_msg ("not attempted, as it has a spec and no definition\
-                           \ (possibly because of DONT_TRANSLATE)");
-             (Binaryset.add(failedsofar, fname), lthy))
         end
     end
   exception NoMods of string Binaryset.set

tools/c-parser/testfiles/jiraver464.c

@@ -1,13 +1,13 @@
 int y;
 
 /** DONT_TRANSLATE */
-/** MODIFIES: y
+/** MODIFIES:
     FNSPEC
     f_spec: "\<Gamma> \<turnstile> {s. x_' s < 3} Call f_'proc {s. ret__int_' s < 3}"
 */
 int f(int x)
 {
-  y++;
+  // y++;
   return x;
 }
 

tools/c-parser/testfiles/jiraver464.thy

@@ -14,13 +14,10 @@ end
 context jiraver464
 begin
   thm f_body_def
+  thm f_modifies
 
-
-lemma f_modifies:
-assumes "x_' \<sigma> < 3"
-shows "\<Gamma>\<turnstile>{\<sigma>} Call f_'proc {t. t may_only_modify_globals \<sigma> in [y]}"
-apply (vcg spec=modifies)
-oops
+thm clz_body_def
+thm clz_modifies
 
 thm clz_body_def
 thm halt_body_def