User:Realazthat/Projects wishlist/LLVM/SMT: Difference between revisions

Content added Content deleted

Inline

@@ Line 36: / Line 36: @@
 '''Example:'''
 <lang llvm>
-%a = alloca i32, align 4                        ; <i32*> [#uses=4]
+%a = alloca i29, align 4                        ; <i29*> [#uses=4]
-%b = alloca i32, align 4                        ; <i32*> [#uses=4]
+%b = alloca i35, align 4                        ; <i35*> [#uses=4]
 </lang>
@@ Line 43: / Line 43: @@
 <pre>
 :extrafuns ((memoryState0 bv[10240]))
-:extrafuns ((stackPtr0 bv[32]))
+:extrafuns ((stackPtr0 bv[16]))
 ;------^^^Initial state ^^^------
-;%a = alloca i32, align 4                        ;; <i32*>
+;%a = alloca i29, align 4                        ;; <i29*>
 :extrafuns ((a bv[16]))                          ; Pointer
-:assumption (= a (bvadd stackPtr0 32))           ; Constraint
+:assumption (= a stackPtr0))                     ; Constraint
-:extrafuns ((stackPtr1 bv[32]))
+:extrafuns ((stackPtr1 bv[16]))
-:assumption (= stackPtr1 (bvadd stackPtr0 32))
+:assumption (= stackPtr1 (bvadd stackPtr0 29))
-;%b = alloca i32, align 4                        ;; <i32*>
+;%b = alloca i35, align 4                        ;; <i35*>
 :extrafuns ((b bv[16]))                          ; Pointer
-:assumption (= b (bvadd stackPtr1 32))           ; Constraint
+:assumption (= b stackPtr1)                      ; Constraint
-:extrafuns ((stackPtr2 bv[32]))                  ; New stack pointer state
+:extrafuns ((stackPtr2 bv[16]))                  ; New stack pointer state
-:assumption (= stackPtr2 (bvadd stackPtr1 32))   ; Constrain new stack pointer
+:assumption (= stackPtr2 (bvadd stackPtr1 35))   ; Constrain new stack pointer
 </pre>