Fixed get_sign.c based on marks feedback

examples/get_sign.c

@@ -177,13 +177,13 @@ int main()
 // Did the result correspond to the expected path for the test?
 //
 // [your answer here]
-// Yes
-// echo $?  gives 255 (which is equal to -1 of 8 signed bits)
+// No
+// echo $?  gives 255 
 //
 // Why not? Confer to shell error codes:
 //
 // [your answer here]
-// ??? TODO
+// In bash exit code 255 means "Exit status out of range" and it says "exit takes only integer args in the range 0 - 255". The result should have been -1 but it is out of range for bash, so that is why I didn't get the expected result.
 //
 // D) Debugging
 //

examples/klee-last

-/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-0
+/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-1
\ No newline at end of file

examples/klee-out-1/assembly.ll

+; ModuleID = 'get_sign.bc'
+source_filename = "get_sign.c"
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @get_sign(i32 %0) #0 {
+  %2 = alloca i32, align 4
+  %3 = alloca i32, align 4
+  store i32 %0, i32* %3, align 4
+  %4 = load i32, i32* %3, align 4
+  %5 = icmp eq i32 %4, 0
+  br i1 %5, label %6, label %7
+
+6:                                                ; preds = %1
+  store i32 0, i32* %2, align 4
+  br label %12
+
+7:                                                ; preds = %1
+  %8 = load i32, i32* %3, align 4
+  %9 = icmp slt i32 %8, 0
+  br i1 %9, label %10, label %11
+
+10:                                               ; preds = %7
+  store i32 -1, i32* %2, align 4
+  br label %12
+
+11:                                               ; preds = %7
+  store i32 1, i32* %2, align 4
+  br label %12
+
+12:                                               ; preds = %11, %10, %6
+  %13 = load i32, i32* %2, align 4
+  ret i32 %13
+}
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @main() #0 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  %3 = bitcast i32* %2 to i8*
+  call void @klee_make_symbolic(i8* %3, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))
+  %4 = load i32, i32* %2, align 4
+  %5 = call i32 @get_sign(i32 %4)
+  ret i32 %5
+}
+
+declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1
+
+attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+
+!llvm.module.flags = !{!0}
+!llvm.ident = !{!1}
+
+!0 = !{i32 1, !"wchar_size", i32 4}
+!1 = !{!"Ubuntu clang version 11.0.0-2"}

examples/klee-out-1/info

+klee get_sign.bc
+PID: 232064
+Using monotonic steady clock with 1/1000000000s resolution
+Started: 2020-12-15 16:48:54
+BEGIN searcher description
+<InterleavedSearcher> containing 2 searchers:
+RandomPathSearcher
+WeightedRandomSearcher::CoveringNew
+</InterleavedSearcher>
+END searcher description
+Finished: 2020-12-15 16:48:54
+Elapsed: 00:00:00
+KLEE: done: explored paths = 3
+KLEE: done: avg. constructs per query = 11
+KLEE: done: total queries = 3
+KLEE: done: valid queries = 0
+KLEE: done: invalid queries = 3
+KLEE: done: query cex = 3
+
+KLEE: done: total instructions = 31
+KLEE: done: completed paths = 3
+KLEE: done: generated tests = 3

examples/klee-out-1/messages.txt

+KLEE: Using Z3 solver backend

examples/klee-out-1/run.istats

+version: 1
+creator: klee
+pid: 232064
+cmd: get_sign.bc
+
+
+positions: instr line
+event: Icov : CoveredInstructions
+event: Forks : Forks
+event: Ireal : InstructionRealTimes
+event: Itime : InstructionTimes
+event: I : Instructions
+event: UCdist : MinDistToUncovered
+event: Rtime : ResolveTime
+event: States : States
+event: Iuncov : UncoveredInstructions
+event: Q : Queries
+event: Qiv : QueriesInvalid
+event: Qv : QueriesValid
+event: Qtime : QueryTime
+events: Icov Forks Ireal Itime I UCdist Rtime States Iuncov Q Qiv Qv Qtime 
+ob=assembly.ll
+fn=get_sign
+10 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+11 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+12 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+13 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+14 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+15 0 1 1 0 0 1 0 0 0 0 2 2 0 32370 
+18 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+19 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+22 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+23 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+24 0 1 1 0 0 1 0 0 0 0 1 1 0 13814 
+27 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+28 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+31 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+32 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+35 0 1 0 0 0 3 0 0 0 0 0 0 0 0 
+36 0 1 0 0 0 3 0 0 0 0 0 0 0 0 
+fn=main
+41 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+42 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+43 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+44 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+45 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+46 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+47 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+cfn=get_sign
+calls=1 8 0
+47 0 17 2 0 0 21 0 0 0 0 3 3 0 46184 
+48 0 1 0 0 0 3 0 0 0 0 0 0 0 0