From 0bbc8657d7b34b3fd7384144d50334435937a641 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 19 Jan 2021 10:16:15 +0100
Subject: [PATCH] [wp] Cosmetic change
---
src/plugins/wp/Cvalues.ml | 11 ++++-------
1 file changed, 4 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index df578509530..5b783c96830 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -147,11 +147,9 @@ module OPAQUE_COMP_BYTES_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
Wp_parameters.fatal
"Asking for opaque struct length on non opaque struct" ;
let result = Lang.t_int in
- let name = "BytesLength" in
- let size =
- Lang.(generated_f ~params:[] ~result "%s_of_%s" name (comp_id c))
- in
- (* Registration *)
+ let f_name = "BytesLength_of_" ^ (comp_id c) in
+ let l_name = "Positive_" ^ f_name in
+ let size = Lang.generated_f ~params:[] ~result "%s" f_name in
Definitions.define_symbol {
d_cluster = Definitions.compinfo c ;
d_lfun = size ; d_types = 0 ; d_params = [] ;
@@ -159,8 +157,7 @@ module OPAQUE_COMP_BYTES_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
} ;
let min_size = if Cil.acceptEmptyCompinfo () then e_zero else e_one in
Definitions.define_lemma {
- l_kind = `Axiom ;
- l_name = "Positive_" ^ name ^ "_of_" ^ Lang.comp_id c ;
+ l_kind = `Axiom ; l_name ;
l_types = 0 ; l_triggers = [] ; l_forall = [] ;
l_cluster = Definitions.compinfo c ;
l_lemma = Lang.F.(p_leq min_size (e_fun size []))
--
GitLab