From e888fc2e65ec464223430b7ad3be1e28795e8b99 Mon Sep 17 00:00:00 2001 From: zhouxuan009 Date: Sun, 28 Mar 2021 15:31:28 +0800 Subject: [PATCH] solve issue #306 --- vsa/value_set/lib/src/cbat_vsa.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/vsa/value_set/lib/src/cbat_vsa.ml b/vsa/value_set/lib/src/cbat_vsa.ml index 5e299473..65ecd4a1 100644 --- a/vsa/value_set/lib/src/cbat_vsa.ml +++ b/vsa/value_set/lib/src/cbat_vsa.ml @@ -388,6 +388,8 @@ let denote_jump (denote_call : sub:tid -> AI.t -> target:tid -> AI.t) *) let denote_block (denote_call : sub:tid -> AI.t -> target:tid -> AI.t) (ctx : program term) ~(source : tid) (env : AI.t) : target:tid -> AI.t = + let source_str = Tid.name source in + if (String.compare source_str "@start-pseudo-node") = 0 || (String.compare source_str "@exit-pseudo-node") = 0 then fun ~target->AI.bottom else match (Program.lookup blk_t ctx source) with | Some b -> let postcond = denote_defs b env in