Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/machine_code.ml | ||
---|---|---|
43 | 43 |
is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals); |
44 | 44 |
get_var = |
45 | 45 |
(fun id -> |
46 |
try List.find (fun v -> v.var_id = id) all |
|
47 |
with Not_found -> |
|
46 |
try List.find (fun v -> v.var_id = id) all
|
|
47 |
with Not_found ->
|
|
48 | 48 |
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id |
49 | 49 |
* VSet.pp all; *) |
50 | 50 |
raise Not_found); |
... | ... | |
373 | 373 |
else mkinstr (MSetReset inst) :: ctx.si); |
374 | 374 |
} |
375 | 375 |
| [ x ], _ -> |
376 |
begin try |
|
376 | 377 |
let var_x = env.get_var x in |
377 | 378 |
let instr, spec = translate_act (var_x, eq.eq_rhs) in |
378 | 379 |
control_on_clock eq.eq_rhs.expr_clock instr True spec ctx |
380 |
with Not_found -> |
|
381 |
Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq ; |
|
382 |
raise Not_found |
|
383 |
end |
|
379 | 384 |
| _ -> |
380 | 385 |
Format.eprintf |
381 | 386 |
"internal error: Machine_code.translate_eq %a@?" |
... | ... | |
484 | 489 |
tname = nd; |
485 | 490 |
tindex = Some 0; |
486 | 491 |
tvars = nd.node_inputs; |
487 |
tformula = True;
|
|
492 |
tformula = if fst (get_stateless_status_node nd) then True else StateVarPack ResetFlag;
|
|
488 | 493 |
tmem_footprint = ISet.empty; |
489 | 494 |
tinst_footprint = IMap.empty; |
490 | 495 |
} |
... | ... | |
508 | 513 |
} |
509 | 514 |
|
510 | 515 |
let translate_eexpr env e = |
516 |
try |
|
511 | 517 |
List.fold_right (fun (qt, xs) f -> match qt with |
512 | 518 |
| Lustre_types.Exists -> Exists (xs, f) |
513 | 519 |
| Lustre_types.Forall -> Forall (xs, f)) |
514 | 520 |
e.eexpr_quantifiers |
515 | 521 |
(Value (translate_expr env e.eexpr_qfexpr)) |
522 |
with |
|
523 |
NormalizationError -> |
|
524 |
Format.eprintf |
|
525 |
"Normalization error: %a@." |
|
526 |
Printers.pp_eexpr |
|
527 |
e; |
|
528 |
raise NormalizationError |
|
529 |
|
|
516 | 530 |
|
517 | 531 |
let translate_contract env c = { |
518 | 532 |
mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume); |
519 |
mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees) |
|
533 |
mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees); |
|
534 |
mc_proof = c.proof |
|
520 | 535 |
} |
521 | 536 |
|
522 | 537 |
let translate_spec env = function |
523 | 538 |
| Contract c -> |
524 | 539 |
Contract (translate_contract env c) |
525 |
| NodeSpec (s, c) ->
|
|
526 |
NodeSpec (s, option_map (translate_contract env) c)
|
|
540 |
| NodeSpec s ->
|
|
541 |
NodeSpec s
|
|
527 | 542 |
|
528 | 543 |
let translate_decl nd sch = |
529 | 544 |
(* Format.eprintf "Translating node %s@." nd.node_id; *) |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example