From c286acff67405058eae4cf5e2243b9958f35e5b8 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 10 Feb 2021 13:31:46 +0100
Subject: [PATCH] small tweaks to container of examples
---
examples/container_of.c | 4 +-
examples/proofs/container_of/generated_code.v | 59 +++++++++----------
2 files changed, 31 insertions(+), 32 deletions(-)
diff --git a/examples/container_of.c b/examples/container_of.c
index a198a1aa..0e606918 100644
--- a/examples/container_of.c
+++ b/examples/container_of.c
@@ -1,5 +1,5 @@
-#define container_of(ptr, type, member) (type *)( (char *)(ptr) - offsetof(type,member) )
+#define container_of(ptr, type, member) (type *)( (unsigned char *)(ptr) - offsetof(type,member) )
struct test {
int a;
@@ -13,5 +13,5 @@ int container_of_test() {
*b = 3;
struct test *pt = container_of(b, struct test, b);
pt->a = 4;
- return pt->a;
+ return t.a;
}
diff --git a/examples/proofs/container_of/generated_code.v b/examples/proofs/container_of/generated_code.v
index d70efdf7..96ae6884 100644
--- a/examples/proofs/container_of/generated_code.v
+++ b/examples/proofs/container_of/generated_code.v
@@ -11,30 +11,29 @@ Section code.
Definition loc_4 : location_info := LocationInfo file_0 13 2 13 9.
Definition loc_5 : location_info := LocationInfo file_0 14 2 14 77.
Definition loc_6 : location_info := LocationInfo file_0 15 2 15 12.
- Definition loc_7 : location_info := LocationInfo file_0 16 2 16 15.
- Definition loc_8 : location_info := LocationInfo file_0 16 9 16 14.
- Definition loc_9 : location_info := LocationInfo file_0 16 9 16 14.
- Definition loc_10 : location_info := LocationInfo file_0 16 9 16 11.
- Definition loc_11 : location_info := LocationInfo file_0 16 9 16 11.
- Definition loc_12 : location_info := LocationInfo file_0 15 2 15 7.
+ Definition loc_7 : location_info := LocationInfo file_0 16 2 16 13.
+ Definition loc_8 : location_info := LocationInfo file_0 16 9 16 12.
+ Definition loc_9 : location_info := LocationInfo file_0 16 9 16 12.
+ Definition loc_10 : location_info := LocationInfo file_0 16 9 16 10.
+ Definition loc_11 : location_info := LocationInfo file_0 15 2 15 7.
+ Definition loc_12 : location_info := LocationInfo file_0 15 2 15 4.
Definition loc_13 : location_info := LocationInfo file_0 15 2 15 4.
- Definition loc_14 : location_info := LocationInfo file_0 15 2 15 4.
- Definition loc_15 : location_info := LocationInfo file_0 15 10 15 11.
- Definition loc_16 : location_info := LocationInfo file_0 14 20 14 76.
- Definition loc_17 : location_info := LocationInfo file_0 14 35 14 76.
- Definition loc_18 : location_info := LocationInfo file_0 14 37 14 48.
+ Definition loc_14 : location_info := LocationInfo file_0 15 10 15 11.
+ Definition loc_15 : location_info := LocationInfo file_0 14 20 14 76.
+ Definition loc_16 : location_info := LocationInfo file_0 14 35 14 76.
+ Definition loc_17 : location_info := LocationInfo file_0 14 37 14 48.
+ Definition loc_18 : location_info := LocationInfo file_0 14 45 14 48.
Definition loc_19 : location_info := LocationInfo file_0 14 45 14 48.
- Definition loc_20 : location_info := LocationInfo file_0 14 45 14 48.
- Definition loc_21 : location_info := LocationInfo file_0 14 51 14 74.
- Definition loc_24 : location_info := LocationInfo file_0 13 2 13 4.
+ Definition loc_20 : location_info := LocationInfo file_0 14 51 14 74.
+ Definition loc_23 : location_info := LocationInfo file_0 13 2 13 4.
+ Definition loc_24 : location_info := LocationInfo file_0 13 3 13 4.
Definition loc_25 : location_info := LocationInfo file_0 13 3 13 4.
- Definition loc_26 : location_info := LocationInfo file_0 13 3 13 4.
- Definition loc_27 : location_info := LocationInfo file_0 13 7 13 8.
- Definition loc_28 : location_info := LocationInfo file_0 12 11 12 15.
- Definition loc_29 : location_info := LocationInfo file_0 12 12 12 15.
- Definition loc_30 : location_info := LocationInfo file_0 12 12 12 13.
- Definition loc_34 : location_info := LocationInfo file_0 11 24 11 25.
- Definition loc_35 : location_info := LocationInfo file_0 11 32 11 33.
+ Definition loc_26 : location_info := LocationInfo file_0 13 7 13 8.
+ Definition loc_27 : location_info := LocationInfo file_0 12 11 12 15.
+ Definition loc_28 : location_info := LocationInfo file_0 12 12 12 15.
+ Definition loc_29 : location_info := LocationInfo file_0 12 12 12 13.
+ Definition loc_33 : location_info := LocationInfo file_0 11 24 11 25.
+ Definition loc_34 : location_info := LocationInfo file_0 11 32 11 33.
(* Definition of struct [test]. *)
Program Definition struct_test := {|
@@ -59,21 +58,21 @@ Section code.
<[ "#0" :=
"t" <-{ layout_of struct_test }
StructInit struct_test [
- ("a", LocInfoE loc_34 (i2v 1 i32) : expr) ;
- ("b", LocInfoE loc_35 (i2v 2 i32) : expr)
+ ("a", LocInfoE loc_33 (i2v 1 i32) : expr) ;
+ ("b", LocInfoE loc_34 (i2v 2 i32) : expr)
] ;
"b" <-{ void* }
- LocInfoE loc_28 (&(LocInfoE loc_29 ((LocInfoE loc_30 ("t")) at{struct_test} "b"))) ;
+ LocInfoE loc_27 (&(LocInfoE loc_28 ((LocInfoE loc_29 ("t")) at{struct_test} "b"))) ;
locinfo: loc_4 ;
- LocInfoE loc_25 (!{void*} (LocInfoE loc_26 ("b"))) <-{ it_layout i32 }
- LocInfoE loc_27 (i2v 3 i32) ;
+ LocInfoE loc_24 (!{void*} (LocInfoE loc_25 ("b"))) <-{ it_layout i32 }
+ LocInfoE loc_26 (i2v 3 i32) ;
"pt" <-{ void* }
- LocInfoE loc_16 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_17 ((LocInfoE loc_18 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_19 (use{void*} (LocInfoE loc_20 ("b")))))) at_neg_offset{it_layout u8, PtrOp, IntOp size_t} (LocInfoE loc_21 ((OffsetOf (struct_test) ("b"))))))) ;
+ LocInfoE loc_15 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_16 ((LocInfoE loc_17 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_18 (use{void*} (LocInfoE loc_19 ("b")))))) at_neg_offset{it_layout u8, PtrOp, IntOp size_t} (LocInfoE loc_20 ((OffsetOf (struct_test) ("b"))))))) ;
locinfo: loc_6 ;
- LocInfoE loc_12 ((LocInfoE loc_13 (!{void*} (LocInfoE loc_14 ("pt")))) at{struct_test} "a") <-{ it_layout i32 }
- LocInfoE loc_15 (i2v 4 i32) ;
+ LocInfoE loc_11 ((LocInfoE loc_12 (!{void*} (LocInfoE loc_13 ("pt")))) at{struct_test} "a") <-{ it_layout i32 }
+ LocInfoE loc_14 (i2v 4 i32) ;
locinfo: loc_7 ;
- Return (LocInfoE loc_8 (use{it_layout i32} (LocInfoE loc_9 ((LocInfoE loc_10 (!{void*} (LocInfoE loc_11 ("pt")))) at{struct_test} "a"))))
+ Return (LocInfoE loc_8 (use{it_layout i32} (LocInfoE loc_9 ((LocInfoE loc_10 ("t")) at{struct_test} "a"))))
]> $∅
)%E
|}.
--
GitLab