Commit 0dc98cd9 authored by Joachim Bard's avatar Joachim Bard

hot fix for floverParser

parent 623980fa
......@@ -309,10 +309,10 @@ Definition parseIV (input:list Token) :option (intv * list Token) :=
| _ => None
end.
Definition defaultPre :(nat -> intv):= fun x => mkIntv 0 0.
Definition defaultPre : precond := FloverMap.empty intv.
Definition updPre (n:nat) (iv:intv) (P:precond) :=
fun m => if (n =? m) then iv else P m.
Definition updPre (n:nat) (iv:intv) (P:precond) : precond :=
FloverMap.add (Var Q n) iv P.
(** Precondition parser:
The precondition should be encoded in the following format:
......@@ -411,6 +411,15 @@ Definition parseGamma (input:list Token) :=
| _ => None
end.
Definition defaultQuerymap := FloverMap.empty (SMTLogic * SMTLogic).
Definition updQuerymap e (ql qr: SMTLogic) Qmap :=
FloverMap.add e (ql, qr) Qmap.
(* TODO: parse the queries properly *)
Definition parseQuerymap (input: list Token) :=
Some (defaultQuerymap, input).
Definition dParse (input:list Token) fuel :=
let cmdParse :=
match input with
......@@ -430,7 +439,11 @@ Definition dParse (input:list Token) fuel :=
| Some (P, absenvRest) =>
match parseAbsEnv absenvRest fuel with
| None => None
| Some (A, residual) => Some ((dCmd, P, A, Gamma), residual)
| Some (A, querymapRest) =>
match parseQuerymap querymapRest with
| None => None
| Some (Qmap, residual) => Some ((dCmd, P, A, Qmap, Gamma), residual)
end
end
end
end
......@@ -442,9 +455,9 @@ Fixpoint str_length s :=
|"" => O
end.
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Qmap Gamma (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
|S n' => CertificateCheckerCmd f A P Qmap Gamma && (check f P A Qmap Gamma n')
|_ => true
end.
......@@ -452,8 +465,8 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
match num_fun with
|S nf =>
match (dParse input fuel) with
|Some ((f,P,A, Gamma), residual) =>
if (check f P A Gamma iters)
|Some ((f,P,A,Qmap,Gamma), residual) =>
if (check f P A Qmap Gamma iters)
then
match residual with
|a :: b => check_all nf iters residual fuel
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment