diff --git a/.gitignore b/.gitignore index a0ee758d6fa..4b04c4fe498 100644 --- a/.gitignore +++ b/.gitignore @@ -112,3 +112,6 @@ src/util/irep_ids_convert src/util/irep_ids_convert.exe *.pyc + +# auto generated documentation +doc/html/ diff --git a/CHANGELOG b/CHANGELOG index 44ac745be0d..e497b1cadc2 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -8,6 +8,8 @@ * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false * GOTO-INSTRUMENT: New option --remove-function-body +* GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to + --no-system-headers 5.7 diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc index bfe77ab09ad..6f55a0d2bc6 100644 --- a/regression/cbmc-java/LocalVarTable5/test.desc +++ b/regression/cbmc-java/LocalVarTable5/test.desc @@ -4,7 +4,7 @@ test.class dead anonlocal::1i dead anonlocal::2i dead anonlocal::3a -dead new_tmp0 +dead new_tmp[0-9]+ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc-java/array2/test.class b/regression/cbmc-java/array2/test.class new file mode 100644 index 00000000000..507d6622e5c Binary files /dev/null and b/regression/cbmc-java/array2/test.class differ diff --git a/regression/cbmc-java/array2/test.desc b/regression/cbmc-java/array2/test.desc new file mode 100644 index 00000000000..6d2226bb26b --- /dev/null +++ b/regression/cbmc-java/array2/test.desc @@ -0,0 +1,6 @@ +CORE +test.class +--function test.f --cover location +\d+ of \d+ covered +-- +^warning: ignoring diff --git a/regression/cbmc-java/array2/test.java b/regression/cbmc-java/array2/test.java new file mode 100644 index 00000000000..075017405ee --- /dev/null +++ b/regression/cbmc-java/array2/test.java @@ -0,0 +1,16 @@ +public class test { + + public void f(int unknown) { + + int[] arr; + if(unknown > 0) + arr = new int[1]; + else + arr = new int[0]; + + if(unknown > 0) + arr[0]=1; + + } + +} diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc index 53856821b22..32dea0b83f5 100644 --- a/regression/cbmc-java/destructor1/test.desc +++ b/regression/cbmc-java/destructor1/test.desc @@ -5,4 +5,4 @@ Break.class ^SIGNAL=0$ dead i; -- -GOTO 10 +GOTO 11 diff --git a/regression/cbmc-java/integer_without_simplify1/test.class b/regression/cbmc-java/integer_without_simplify1/test.class new file mode 100644 index 00000000000..1ee5d36d95a Binary files /dev/null and b/regression/cbmc-java/integer_without_simplify1/test.class differ diff --git a/regression/cbmc-java/integer_without_simplify1/test.desc b/regression/cbmc-java/integer_without_simplify1/test.desc new file mode 100644 index 00000000000..284277c7b4a --- /dev/null +++ b/regression/cbmc-java/integer_without_simplify1/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +--no-simplify --function test.f --cover location +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/integer_without_simplify1/test.java b/regression/cbmc-java/integer_without_simplify1/test.java new file mode 100644 index 00000000000..62b2060b7c0 --- /dev/null +++ b/regression/cbmc-java/integer_without_simplify1/test.java @@ -0,0 +1,10 @@ + +public class test { + + public void f() { + + int x = 50; + + } + +} diff --git a/regression/cbmc-java/stack_var1/README b/regression/cbmc-java/stack_var1/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var1/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var1/stack_test.class b/regression/cbmc-java/stack_var1/stack_test.class new file mode 100644 index 00000000000..2b723f49df8 Binary files /dev/null and b/regression/cbmc-java/stack_var1/stack_test.class differ diff --git a/regression/cbmc-java/stack_var1/stack_test.java b/regression/cbmc-java/stack_var1/stack_test.java new file mode 100644 index 00000000000..cb404e89473 --- /dev/null +++ b/regression/cbmc-java/stack_var1/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var1 s = new stack_var1(); + int n = s.f(1); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var1/stack_var1.class b/regression/cbmc-java/stack_var1/stack_var1.class new file mode 100644 index 00000000000..67a2f733081 Binary files /dev/null and b/regression/cbmc-java/stack_var1/stack_var1.class differ diff --git a/regression/cbmc-java/stack_var1/stack_var1.j b/regression/cbmc-java/stack_var1/stack_var1.j new file mode 100644 index 00000000000..a3736df18e2 --- /dev/null +++ b/regression/cbmc-java/stack_var1/stack_var1.j @@ -0,0 +1,22 @@ +.class public stack_var1 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f(I)I + .limit stack 2 + .limit locals 2 + + ;; copy of arg on stack + iload_1 + ;; increment arg + iinc 1 1 + ;; incremented copy on stack + iload_1 + isub + ireturn +.end method diff --git a/regression/cbmc-java/stack_var1/test.desc b/regression/cbmc-java/stack_var1/test.desc new file mode 100644 index 00000000000..3bf59401a5a --- /dev/null +++ b/regression/cbmc-java/stack_var1/test.desc @@ -0,0 +1,9 @@ +CORE +stack_test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var10/README b/regression/cbmc-java/stack_var10/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var10/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var10/stack_test.class b/regression/cbmc-java/stack_var10/stack_test.class new file mode 100644 index 00000000000..09a5b5a8de9 Binary files /dev/null and b/regression/cbmc-java/stack_var10/stack_test.class differ diff --git a/regression/cbmc-java/stack_var10/stack_test.java b/regression/cbmc-java/stack_var10/stack_test.java new file mode 100644 index 00000000000..3831ddea4ab --- /dev/null +++ b/regression/cbmc-java/stack_var10/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var10 s = new stack_var10(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var10/stack_var10.class b/regression/cbmc-java/stack_var10/stack_var10.class new file mode 100644 index 00000000000..68bab7d3abd Binary files /dev/null and b/regression/cbmc-java/stack_var10/stack_var10.class differ diff --git a/regression/cbmc-java/stack_var10/stack_var10.j b/regression/cbmc-java/stack_var10/stack_var10.j new file mode 100644 index 00000000000..0d6fe63957f --- /dev/null +++ b/regression/cbmc-java/stack_var10/stack_var10.j @@ -0,0 +1,28 @@ +.class public stack_var10 +.super java/lang/Object + +.field private static n I + +.method public ()V +.limit stack 5 + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()I + .limit stack 8 + .limit locals 5 + + iconst_1 + istore_1 + iconst_0 + istore_2 + ;; lvar1 is 1, lvar2 is 0 + iload_1 + iload_2 + ;; on stack 1, 0 + istore_1 + ;; store 0 into lvar1 + ireturn +.end method diff --git a/regression/cbmc-java/stack_var10/test.desc b/regression/cbmc-java/stack_var10/test.desc new file mode 100644 index 00000000000..3bf59401a5a --- /dev/null +++ b/regression/cbmc-java/stack_var10/test.desc @@ -0,0 +1,9 @@ +CORE +stack_test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var11/README b/regression/cbmc-java/stack_var11/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var11/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var11/stack_test.class b/regression/cbmc-java/stack_var11/stack_test.class new file mode 100644 index 00000000000..3d46a551ddc Binary files /dev/null and b/regression/cbmc-java/stack_var11/stack_test.class differ diff --git a/regression/cbmc-java/stack_var11/stack_test.java b/regression/cbmc-java/stack_var11/stack_test.java new file mode 100644 index 00000000000..59c979f849b --- /dev/null +++ b/regression/cbmc-java/stack_var11/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var11 s = new stack_var11(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var11/stack_var11.class b/regression/cbmc-java/stack_var11/stack_var11.class new file mode 100644 index 00000000000..a19f186ab03 Binary files /dev/null and b/regression/cbmc-java/stack_var11/stack_var11.class differ diff --git a/regression/cbmc-java/stack_var11/stack_var11.j b/regression/cbmc-java/stack_var11/stack_var11.j new file mode 100644 index 00000000000..16818a4a4e3 --- /dev/null +++ b/regression/cbmc-java/stack_var11/stack_var11.j @@ -0,0 +1,31 @@ +.class public stack_var11 +.super java/lang/Object + +.field private arr [I + +.method public ()V +.limit stack 5 + aload_0 + invokenonvirtual java/lang/Object/()V + aload_0 + iconst_2 + newarray int + putfield stack_var11/arr [I + return +.end method + +.method public f()I + .limit stack 8 + .limit locals 5 + aload_0 + getfield stack_var11/arr [I + iconst_0 + iaload ;; put arr[0] on stack (currently 0) + aload_0 + getfield stack_var11/arr [I + iconst_0 + iconst_1 + iastore ;; store 1 in arr[0], + ;; value on stack should not be touched + ireturn +.end method diff --git a/regression/cbmc-java/stack_var2/README b/regression/cbmc-java/stack_var2/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var2/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var2/stack_test.class b/regression/cbmc-java/stack_var2/stack_test.class new file mode 100644 index 00000000000..f26c64d43d4 Binary files /dev/null and b/regression/cbmc-java/stack_var2/stack_test.class differ diff --git a/regression/cbmc-java/stack_var2/stack_test.java b/regression/cbmc-java/stack_var2/stack_test.java new file mode 100644 index 00000000000..822716f691c --- /dev/null +++ b/regression/cbmc-java/stack_var2/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var2 s = new stack_var2(); + int n = s.f(1); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var2/stack_var2.class b/regression/cbmc-java/stack_var2/stack_var2.class new file mode 100644 index 00000000000..6db13604864 Binary files /dev/null and b/regression/cbmc-java/stack_var2/stack_var2.class differ diff --git a/regression/cbmc-java/stack_var2/stack_var2.j b/regression/cbmc-java/stack_var2/stack_var2.j new file mode 100644 index 00000000000..e20a174070c --- /dev/null +++ b/regression/cbmc-java/stack_var2/stack_var2.j @@ -0,0 +1,25 @@ +.class public stack_var2 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f(I)I + .limit stack 3 + .limit locals 2 + + ;; push local var1 + iload_1 + ;; duplicate + dup + ;; increment local var1 + iinc 1 1 + ;; push local var1 + iload_1 + isub + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var2/test.desc b/regression/cbmc-java/stack_var2/test.desc new file mode 100644 index 00000000000..3bf59401a5a --- /dev/null +++ b/regression/cbmc-java/stack_var2/test.desc @@ -0,0 +1,9 @@ +CORE +stack_test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var3/README b/regression/cbmc-java/stack_var3/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var3/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var3/stack_test.class b/regression/cbmc-java/stack_var3/stack_test.class new file mode 100644 index 00000000000..a42cc9101a1 Binary files /dev/null and b/regression/cbmc-java/stack_var3/stack_test.class differ diff --git a/regression/cbmc-java/stack_var3/stack_test.java b/regression/cbmc-java/stack_var3/stack_test.java new file mode 100644 index 00000000000..7ffc016070c --- /dev/null +++ b/regression/cbmc-java/stack_var3/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var3 s = new stack_var3(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var3/stack_var3.class b/regression/cbmc-java/stack_var3/stack_var3.class new file mode 100644 index 00000000000..9a3a0d6d370 Binary files /dev/null and b/regression/cbmc-java/stack_var3/stack_var3.class differ diff --git a/regression/cbmc-java/stack_var3/stack_var3.j b/regression/cbmc-java/stack_var3/stack_var3.j new file mode 100644 index 00000000000..f215d15b4bc --- /dev/null +++ b/regression/cbmc-java/stack_var3/stack_var3.j @@ -0,0 +1,33 @@ +.class public stack_var3 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()I + .limit stack 5 + .limit locals 3 + + ;; 1->var1 + ;; 0->var2 + iconst_1 + istore_1 + iconst_0 + istore_2 + ;; push local var2 / var1 + iload_2 + iload_1 + ;; dup var1 + dup_x1 + ;; sub one from var1 + iinc 1 -1 + ;; pop first var1 + pop + ;; sub + isub + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var3/test.desc b/regression/cbmc-java/stack_var3/test.desc new file mode 100644 index 00000000000..3bf59401a5a --- /dev/null +++ b/regression/cbmc-java/stack_var3/test.desc @@ -0,0 +1,9 @@ +CORE +stack_test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var4/README b/regression/cbmc-java/stack_var4/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var4/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var4/stack_test.class b/regression/cbmc-java/stack_var4/stack_test.class new file mode 100644 index 00000000000..cfbb80f78e8 Binary files /dev/null and b/regression/cbmc-java/stack_var4/stack_test.class differ diff --git a/regression/cbmc-java/stack_var4/stack_test.java b/regression/cbmc-java/stack_var4/stack_test.java new file mode 100644 index 00000000000..1088dd5ac2e --- /dev/null +++ b/regression/cbmc-java/stack_var4/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var4 s = new stack_var4(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var4/stack_var4.class b/regression/cbmc-java/stack_var4/stack_var4.class new file mode 100644 index 00000000000..782443dd6e3 Binary files /dev/null and b/regression/cbmc-java/stack_var4/stack_var4.class differ diff --git a/regression/cbmc-java/stack_var4/stack_var4.j b/regression/cbmc-java/stack_var4/stack_var4.j new file mode 100644 index 00000000000..99eecf3794a --- /dev/null +++ b/regression/cbmc-java/stack_var4/stack_var4.j @@ -0,0 +1,37 @@ +.class public stack_var4 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()I + .limit stack 5 + .limit locals 4 + + ;; 0->var1 + ;; 1->var2 + ;; 2->var3 + iconst_0 + istore_1 + iconst_1 + istore_2 + iconst_2 + istore_3 + + ;; push local var3 / var2 / var1 + iload_3 + iload_2 + iload_1 + ;; push var1 in front of var3 + dup_x2 + ;; add one to local var 1 + iinc 1 1 + pop + pop + pop + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var4/test.desc b/regression/cbmc-java/stack_var4/test.desc new file mode 100644 index 00000000000..805e44acccd --- /dev/null +++ b/regression/cbmc-java/stack_var4/test.desc @@ -0,0 +1,10 @@ +CORE +stack_test.class + +^EXIT=0$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: SUCCESS +$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var5/README b/regression/cbmc-java/stack_var5/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var5/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var5/stack_test.class b/regression/cbmc-java/stack_var5/stack_test.class new file mode 100644 index 00000000000..57cf43dac86 Binary files /dev/null and b/regression/cbmc-java/stack_var5/stack_test.class differ diff --git a/regression/cbmc-java/stack_var5/stack_test.java b/regression/cbmc-java/stack_var5/stack_test.java new file mode 100644 index 00000000000..bfcbe79325d --- /dev/null +++ b/regression/cbmc-java/stack_var5/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var5 s = new stack_var5(); + int n = s.f(); + assert(n==1); + } +} diff --git a/regression/cbmc-java/stack_var5/stack_var5.class b/regression/cbmc-java/stack_var5/stack_var5.class new file mode 100644 index 00000000000..6230e78a9c7 Binary files /dev/null and b/regression/cbmc-java/stack_var5/stack_var5.class differ diff --git a/regression/cbmc-java/stack_var5/stack_var5.j b/regression/cbmc-java/stack_var5/stack_var5.j new file mode 100644 index 00000000000..0871fb68e0b --- /dev/null +++ b/regression/cbmc-java/stack_var5/stack_var5.j @@ -0,0 +1,33 @@ +.class public stack_var5 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()I + .limit stack 4 + .limit locals 4 + + ;; 1->var1 + ;; 2->var2 + iconst_1 + istore_1 + iconst_2 + istore_2 + + ;; push local var2 / var1 + iload_2 + iload_1 + + ;; duplicate var2 / var1 + dup2 + ;; add one to local var 1 + iinc 1 1 + ;; sub + isub + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var5/test.desc b/regression/cbmc-java/stack_var5/test.desc new file mode 100644 index 00000000000..805e44acccd --- /dev/null +++ b/regression/cbmc-java/stack_var5/test.desc @@ -0,0 +1,10 @@ +CORE +stack_test.class + +^EXIT=0$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: SUCCESS +$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var6/README b/regression/cbmc-java/stack_var6/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var6/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var6/stack_test.class b/regression/cbmc-java/stack_var6/stack_test.class new file mode 100644 index 00000000000..c5e765b667b Binary files /dev/null and b/regression/cbmc-java/stack_var6/stack_test.class differ diff --git a/regression/cbmc-java/stack_var6/stack_test.java b/regression/cbmc-java/stack_var6/stack_test.java new file mode 100644 index 00000000000..392d200d370 --- /dev/null +++ b/regression/cbmc-java/stack_var6/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var6 s = new stack_var6(); + int n = s.f(1,2,4); + assert(n==-2); + } +} diff --git a/regression/cbmc-java/stack_var6/stack_var6.class b/regression/cbmc-java/stack_var6/stack_var6.class new file mode 100644 index 00000000000..05223a9a349 Binary files /dev/null and b/regression/cbmc-java/stack_var6/stack_var6.class differ diff --git a/regression/cbmc-java/stack_var6/stack_var6.j b/regression/cbmc-java/stack_var6/stack_var6.j new file mode 100644 index 00000000000..19108f70e36 --- /dev/null +++ b/regression/cbmc-java/stack_var6/stack_var6.j @@ -0,0 +1,25 @@ +.class public stack_var6 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f(III)I + .limit stack 8 + .limit locals 5 + + ;; push local var3 / var2 / var1 + iload_1 + iload_2 + iload_3 + dup2_x1 + ;; add one to local var 2 + iinc 2 1 + ;; sub + isub + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var6/test.desc b/regression/cbmc-java/stack_var6/test.desc new file mode 100644 index 00000000000..805e44acccd --- /dev/null +++ b/regression/cbmc-java/stack_var6/test.desc @@ -0,0 +1,10 @@ +CORE +stack_test.class + +^EXIT=0$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: SUCCESS +$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var7/README b/regression/cbmc-java/stack_var7/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var7/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var7/stack_test.class b/regression/cbmc-java/stack_var7/stack_test.class new file mode 100644 index 00000000000..21eabe9a029 Binary files /dev/null and b/regression/cbmc-java/stack_var7/stack_test.class differ diff --git a/regression/cbmc-java/stack_var7/stack_test.java b/regression/cbmc-java/stack_var7/stack_test.java new file mode 100644 index 00000000000..b742878507e --- /dev/null +++ b/regression/cbmc-java/stack_var7/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var7 s = new stack_var7(); + int n = s.f(); + assert(n==1); + } +} diff --git a/regression/cbmc-java/stack_var7/stack_var7.class b/regression/cbmc-java/stack_var7/stack_var7.class new file mode 100644 index 00000000000..dcc6f0fc1b6 Binary files /dev/null and b/regression/cbmc-java/stack_var7/stack_var7.class differ diff --git a/regression/cbmc-java/stack_var7/stack_var7.j b/regression/cbmc-java/stack_var7/stack_var7.j new file mode 100644 index 00000000000..e75f96b833d --- /dev/null +++ b/regression/cbmc-java/stack_var7/stack_var7.j @@ -0,0 +1,43 @@ +.class public stack_var7 +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()I + .limit stack 8 + .limit locals 5 + + ;; 1->var1 + ;; 2->var2 + ;; 4->var3 + ;; 8->var4 + iconst_1 + istore_1 + iconst_2 + istore_2 + iconst_4 + istore_3 + bipush 8 + istore 4 + ;; push local var4 / var3 / var2 / var1 + iload 4 + iload_3 + iload_2 + iload 1 + ;; push var2 / var1 in on head + dup2_x2 + ;; add one to local var 1 + iinc 1 1 + pop + pop + pop + pop + ;; sub + isub + ;; incremented copy on stack + ireturn +.end method diff --git a/regression/cbmc-java/stack_var7/test.desc b/regression/cbmc-java/stack_var7/test.desc new file mode 100644 index 00000000000..805e44acccd --- /dev/null +++ b/regression/cbmc-java/stack_var7/test.desc @@ -0,0 +1,10 @@ +CORE +stack_test.class + +^EXIT=0$ +^SIGNAL=0$ +^.*assertion at file stack_test.java line 5 function.*: SUCCESS +$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/stack_var8/README b/regression/cbmc-java/stack_var8/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var8/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var8/stack_test.class b/regression/cbmc-java/stack_var8/stack_test.class new file mode 100644 index 00000000000..8ea61591cbc Binary files /dev/null and b/regression/cbmc-java/stack_var8/stack_test.class differ diff --git a/regression/cbmc-java/stack_var8/stack_test.java b/regression/cbmc-java/stack_var8/stack_test.java new file mode 100644 index 00000000000..3a288890e69 --- /dev/null +++ b/regression/cbmc-java/stack_var8/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var8 s = new stack_var8(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var8/stack_var8.class b/regression/cbmc-java/stack_var8/stack_var8.class new file mode 100644 index 00000000000..5298a7d8c92 Binary files /dev/null and b/regression/cbmc-java/stack_var8/stack_var8.class differ diff --git a/regression/cbmc-java/stack_var8/stack_var8.j b/regression/cbmc-java/stack_var8/stack_var8.j new file mode 100644 index 00000000000..d5bec33279d --- /dev/null +++ b/regression/cbmc-java/stack_var8/stack_var8.j @@ -0,0 +1,27 @@ +.class public stack_var8 +.super java/lang/Object + +.field private n I + +.method public ()V +.limit stack 5 + aload_0 + invokenonvirtual java/lang/Object/()V + aload_0 + iconst_0 + putfield stack_var8/n I + return +.end method + +.method public f()I + .limit stack 8 + .limit locals 5 + + aload_0 + getfield stack_var8/n I + aload_0 + iconst_1 + putfield stack_var8/n I + + ireturn +.end method diff --git a/regression/cbmc-java/stack_var9/README b/regression/cbmc-java/stack_var9/README new file mode 100644 index 00000000000..7a032cccbcd --- /dev/null +++ b/regression/cbmc-java/stack_var9/README @@ -0,0 +1,9 @@ +This regression test is created from the .j file with the jasmin assembler. +https://github.com/Sable/jasmin + +On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is +sufficient to do + +> jasmin $FILE.j + +and it will create the corresponding $FILE.class file. diff --git a/regression/cbmc-java/stack_var9/stack_test.class b/regression/cbmc-java/stack_var9/stack_test.class new file mode 100644 index 00000000000..4f20f14f7d1 Binary files /dev/null and b/regression/cbmc-java/stack_var9/stack_test.class differ diff --git a/regression/cbmc-java/stack_var9/stack_test.java b/regression/cbmc-java/stack_var9/stack_test.java new file mode 100644 index 00000000000..994e7974026 --- /dev/null +++ b/regression/cbmc-java/stack_var9/stack_test.java @@ -0,0 +1,7 @@ +public class stack_test { + public static void main(String[] args) { + stack_var9 s = new stack_var9(); + int n = s.f(); + assert(n==0); + } +} diff --git a/regression/cbmc-java/stack_var9/stack_var9.class b/regression/cbmc-java/stack_var9/stack_var9.class new file mode 100644 index 00000000000..1fa90019a0e Binary files /dev/null and b/regression/cbmc-java/stack_var9/stack_var9.class differ diff --git a/regression/cbmc-java/stack_var9/stack_var9.j b/regression/cbmc-java/stack_var9/stack_var9.j new file mode 100644 index 00000000000..aeee091def0 --- /dev/null +++ b/regression/cbmc-java/stack_var9/stack_var9.j @@ -0,0 +1,24 @@ +.class public stack_var9 +.super java/lang/Object + +.field private static n I + +.method public ()V +.limit stack 5 + aload_0 + invokenonvirtual java/lang/Object/()V + iconst_0 + putstatic stack_var9/n I + return +.end method + +.method public f()I + .limit stack 8 + .limit locals 5 + + getstatic stack_var9/n I + iconst_1 + putstatic stack_var9/n I + + ireturn +.end method diff --git a/regression/cbmc/memset2/main.c b/regression/cbmc/memset2/main.c new file mode 100644 index 00000000000..c317d161215 --- /dev/null +++ b/regression/cbmc/memset2/main.c @@ -0,0 +1,22 @@ +#include +#include + +typedef struct { + int a; + int b; +} TEST; + +static TEST test; + +main() +{ + test.a = 1; + test.b = 2; + memset(&test.b, 0, sizeof(test.b)); + assert(test.a); + assert(!test.b); + test.b = 2; + memset(&test.a, 0, sizeof(test.a)); + assert(!test.a); + assert(test.b); +} diff --git a/regression/cbmc/memset2/test.desc b/regression/cbmc/memset2/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/memset2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/unwind_counters1/main.c b/regression/cbmc/unwind_counters1/main.c new file mode 100644 index 00000000000..6668d3a3914 --- /dev/null +++ b/regression/cbmc/unwind_counters1/main.c @@ -0,0 +1,6 @@ +int main() +{ + for(int i=0; i<2; ++i) + for(int j=0; j<10; ++j); + return 0; +} diff --git a/regression/cbmc/unwind_counters1/test.desc b/regression/cbmc/unwind_counters1/test.desc new file mode 100644 index 00000000000..46efb30683e --- /dev/null +++ b/regression/cbmc/unwind_counters1/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 11 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/unwind_counters2/main.c b/regression/cbmc/unwind_counters2/main.c new file mode 100644 index 00000000000..447015074c9 --- /dev/null +++ b/regression/cbmc/unwind_counters2/main.c @@ -0,0 +1,8 @@ +int main() +{ + l2: goto l1; + l1: int x=5; + goto l2; + + return 0; +} diff --git a/regression/cbmc/unwind_counters2/test.desc b/regression/cbmc/unwind_counters2/test.desc new file mode 100644 index 00000000000..70b64ab793d --- /dev/null +++ b/regression/cbmc/unwind_counters2/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 3 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/cbmc/unwind_counters3/main.c b/regression/cbmc/unwind_counters3/main.c new file mode 100644 index 00000000000..caa1d607594 --- /dev/null +++ b/regression/cbmc/unwind_counters3/main.c @@ -0,0 +1,9 @@ +int main() +{ + int i=0; + l2: if(i==1) int y=0; + l1: int x=5; + goto l2; + + return 0; +} diff --git a/regression/cbmc/unwind_counters3/test.desc b/regression/cbmc/unwind_counters3/test.desc new file mode 100644 index 00000000000..70b64ab793d --- /dev/null +++ b/regression/cbmc/unwind_counters3/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 3 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc index 38027f70600..c0e6ab6bfc2 100644 --- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$ ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index e6f1f4b5752..0d2ddf970da 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index e6f1f4b5752..383f5ad956c 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -5,6 +5,7 @@ main.c ^\s*IF fp == f2 THEN GOTO [0-9]$ ^\s*IF fp == f3 THEN GOTO [0-9]$ ^\s*IF fp == f4 THEN GOTO [0-9]$ +replacing function pointer by 3 possible targets ^SIGNAL=0$ -- ^warning: ignoring @@ -14,3 +15,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index e6f1f4b5752..0d2ddf970da 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index e6f1f4b5752..0d2ddf970da 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index e6f1f4b5752..0d2ddf970da 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index 661ac93a14f..b2f2a12d4ee 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc @@ -14,3 +14,4 @@ main.c ^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$ ^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c new file mode 100644 index 00000000000..bc7c67957e2 --- /dev/null +++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/main.c @@ -0,0 +1,42 @@ +#include + +void f1 (void) { printf("%i\n", 1); } +void f2 (void) { printf("%i\n", 2); } +void f3 (void) { printf("%i\n", 3); } +void f4 (void) { printf("%i\n", 4); } +void f5 (void) { printf("%i\n", 5); } +void f6 (void) { printf("%i\n", 6); } +void f7 (void) { printf("%i\n", 7); } +void f8 (void) { printf("%i\n", 8); } +void f9 (void) { printf("%i\n", 9); } + +typedef void(*void_fp)(void); + +struct action +{ + int x; + void_fp fun; +}; + +// Array with an empty final element +const struct action fp_tbl[5] = {{1, f2}, {2, f3} ,{3, f4},}; + +// There is a basic check that excludes all functions that aren't used anywhere +// This ensures that check can't work in this example +const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9}; + +void func(int i) +{ + const void_fp fp = fp_tbl[i].fun; + fp(); +} + +int main() +{ + for(int i=0;i<3;i++) + { + func(i); + } + + return 0; +} diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc new file mode 100644 index 00000000000..fab84bc077c --- /dev/null +++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--show-goto-functions --verbosity 10 --pointer-check +^Removing function pointers and virtual functions$ +^\s*IF fp == f2 THEN GOTO [0-9]$ +^\s*IF fp == f3 THEN GOTO [0-9]$ +^\s*IF fp == f4 THEN GOTO [0-9]$ +^\s*ASSERT FALSE // invalid function pointer$ +^SIGNAL=0$ +-- +^warning: ignoring +^\s*IF fp == f1 THEN GOTO [0-9]$ +^\s*IF fp == f5 THEN GOTO [0-9]$ +^\s*IF fp == f6 THEN GOTO [0-9]$ +^\s*IF fp == f7 THEN GOTO [0-9]$ +^\s*IF fp == f8 THEN GOTO [0-9]$ +^\s*IF fp == f9 THEN GOTO [0-9]$ +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index 4786993cade..90a60c56a40 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc @@ -4,5 +4,6 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ ^SIGNAL=0$ +function func: replacing function pointer by 0 possible targets -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index 4786993cade..1299353033d 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc @@ -4,5 +4,6 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ ^SIGNAL=0$ +replacing function pointer by 0 possible targets -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index 4786993cade..40a2b941d75 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ +replacing function pointer by 9 possible targets ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index 4786993cade..40a2b941d75 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -3,6 +3,7 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ +replacing function pointer by 9 possible targets ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index d8e8d833238..bea1fb7c356 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -3,5 +3,6 @@ main.c --show-goto-functions --verbosity 10 --pointer-check ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ +function func: replacing function pointer by 0 possible targets -- ^warning: ignoring diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index 4786993cade..1299353033d 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc @@ -4,5 +4,6 @@ main.c ^Removing function pointers and virtual functions$ ^\s*ASSERT FALSE // invalid function pointer$ ^SIGNAL=0$ +replacing function pointer by 0 possible targets -- ^warning: ignoring diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc index ab2a0acefba..bb3ac1b5cf1 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc @@ -5,3 +5,4 @@ main.c ^\s*f3\(\);$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index 90cd2485ce1..153ca97de3b 100644 --- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc index 40361f6ccc2..27df5bd2f67 100644 --- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc index 90cd2485ce1..153ca97de3b 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc index 4dd6e7fd098..402774c29b7 100644 --- a/regression/goto-analyzer/precise-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp/test.desc @@ -5,3 +5,4 @@ main.c ^\s*f2\(\); -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc index 40361f6ccc2..27df5bd2f67 100644 --- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc +++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc index 90cd2485ce1..153ca97de3b 100644 --- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc index 4dd6e7fd098..402774c29b7 100644 --- a/regression/goto-analyzer/precise-derefence/test.desc +++ b/regression/goto-analyzer/precise-derefence/test.desc @@ -5,3 +5,4 @@ main.c ^\s*f2\(\); -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc index fad0e6c7a1d..98fc0ff815c 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc @@ -6,3 +6,4 @@ main.c ^SIGNAL=0$ -- ^warning: ignoring +function \w+: replacing function pointer by 9 possible targets diff --git a/regression/taint/aliasing1/aliasing1.class b/regression/goto-analyzer/taint-aliasing1/aliasing1.class similarity index 100% rename from regression/taint/aliasing1/aliasing1.class rename to regression/goto-analyzer/taint-aliasing1/aliasing1.class diff --git a/regression/taint/aliasing1/aliasing1.java b/regression/goto-analyzer/taint-aliasing1/aliasing1.java similarity index 100% rename from regression/taint/aliasing1/aliasing1.java rename to regression/goto-analyzer/taint-aliasing1/aliasing1.java diff --git a/regression/taint/aliasing1/taint.json b/regression/goto-analyzer/taint-aliasing1/taint.json similarity index 100% rename from regression/taint/aliasing1/taint.json rename to regression/goto-analyzer/taint-aliasing1/taint.json diff --git a/regression/goto-analyzer/taint-aliasing1/test.desc b/regression/goto-analyzer/taint-aliasing1/test.desc new file mode 100644 index 00000000000..49818c9c42b --- /dev/null +++ b/regression/goto-analyzer/taint-aliasing1/test.desc @@ -0,0 +1,9 @@ +CORE +aliasing1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file aliasing1.java line 10( function .*)?: There is a flow \(taint rule my_sink\)$ +-- +^file aliasing1.java line 8( function .*)?: There is a flow \(taint rule my_sink\)$ +^warning: ignoring diff --git a/regression/taint/basic1/basic1.class b/regression/goto-analyzer/taint-basic1/basic1.class similarity index 100% rename from regression/taint/basic1/basic1.class rename to regression/goto-analyzer/taint-basic1/basic1.class diff --git a/regression/taint/basic1/basic1.java b/regression/goto-analyzer/taint-basic1/basic1.java similarity index 100% rename from regression/taint/basic1/basic1.java rename to regression/goto-analyzer/taint-basic1/basic1.java diff --git a/regression/taint/basic1/taint.json b/regression/goto-analyzer/taint-basic1/taint.json similarity index 100% rename from regression/taint/basic1/taint.json rename to regression/goto-analyzer/taint-basic1/taint.json diff --git a/regression/goto-analyzer/taint-basic1/test.desc b/regression/goto-analyzer/taint-basic1/test.desc new file mode 100644 index 00000000000..0da443b9d31 --- /dev/null +++ b/regression/goto-analyzer/taint-basic1/test.desc @@ -0,0 +1,9 @@ +CORE +basic1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file basic1.java line 8( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +^file basic1.java line 11( function .*)?: There is a T2 flow \(taint rule my_h2\)$ +-- +^warning: ignoring diff --git a/regression/taint/basic2/basic2.class b/regression/goto-analyzer/taint-basic2/basic2.class similarity index 100% rename from regression/taint/basic2/basic2.class rename to regression/goto-analyzer/taint-basic2/basic2.class diff --git a/regression/taint/basic2/basic2.java b/regression/goto-analyzer/taint-basic2/basic2.java similarity index 100% rename from regression/taint/basic2/basic2.java rename to regression/goto-analyzer/taint-basic2/basic2.java diff --git a/regression/taint/basic2/taint.json b/regression/goto-analyzer/taint-basic2/taint.json similarity index 100% rename from regression/taint/basic2/taint.json rename to regression/goto-analyzer/taint-basic2/taint.json diff --git a/regression/goto-analyzer/taint-basic2/test.desc b/regression/goto-analyzer/taint-basic2/test.desc new file mode 100644 index 00000000000..b40e010d8f2 --- /dev/null +++ b/regression/goto-analyzer/taint-basic2/test.desc @@ -0,0 +1,9 @@ +CORE +basic2.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file basic2.java line 8( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +^file basic2.java line 11( function .*)?: There is a T2 flow \(taint rule my_h2\)$ +-- +^warning: ignoring diff --git a/regression/taint/interface1/interface1.class b/regression/goto-analyzer/taint-interface1/interface1.class similarity index 97% rename from regression/taint/interface1/interface1.class rename to regression/goto-analyzer/taint-interface1/interface1.class index 31a3578bcdf..056ea5d7b3a 100644 Binary files a/regression/taint/interface1/interface1.class and b/regression/goto-analyzer/taint-interface1/interface1.class differ diff --git a/regression/taint/interface1/interface1.java b/regression/goto-analyzer/taint-interface1/interface1.java similarity index 100% rename from regression/taint/interface1/interface1.java rename to regression/goto-analyzer/taint-interface1/interface1.java diff --git a/regression/goto-analyzer/taint-interface1/my_I.class b/regression/goto-analyzer/taint-interface1/my_I.class new file mode 100644 index 00000000000..f2560c4dda7 Binary files /dev/null and b/regression/goto-analyzer/taint-interface1/my_I.class differ diff --git a/regression/goto-analyzer/taint-interface1/some_class.class b/regression/goto-analyzer/taint-interface1/some_class.class new file mode 100644 index 00000000000..b3261423efd Binary files /dev/null and b/regression/goto-analyzer/taint-interface1/some_class.class differ diff --git a/regression/taint/interface1/taint.json b/regression/goto-analyzer/taint-interface1/taint.json similarity index 100% rename from regression/taint/interface1/taint.json rename to regression/goto-analyzer/taint-interface1/taint.json diff --git a/regression/goto-analyzer/taint-interface1/test.desc b/regression/goto-analyzer/taint-interface1/test.desc new file mode 100644 index 00000000000..bbbbdcd0443 --- /dev/null +++ b/regression/goto-analyzer/taint-interface1/test.desc @@ -0,0 +1,8 @@ +CORE +interface1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file interface1.java line 18( function .*)?: There is a flow! \(taint rule sink_rule\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/taint-interproc1/interproc1.class b/regression/goto-analyzer/taint-interproc1/interproc1.class new file mode 100644 index 00000000000..6d8559b3085 Binary files /dev/null and b/regression/goto-analyzer/taint-interproc1/interproc1.class differ diff --git a/regression/goto-analyzer/taint-interproc1/interproc1.java b/regression/goto-analyzer/taint-interproc1/interproc1.java new file mode 100644 index 00000000000..d092c38a536 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/interproc1.java @@ -0,0 +1,19 @@ +class interproc1 +{ + static void my_method() + { + Object o=null; + + my_f(o); // T1 source + my_g(o); + } + + static void my_g(Object p) + { + my_h(p); // T1 sink + } + + static void my_f(Object p) { } + static void my_h(Object p) { } +}; + diff --git a/regression/goto-analyzer/taint-interproc1/taint.json b/regression/goto-analyzer/taint-interproc1/taint.json new file mode 100644 index 00000000000..26fadfb2775 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/taint.json @@ -0,0 +1,4 @@ +[ +{ "id": "my_f", "kind": "source", "where": "parameter1", "taint": "T1", "function": "interproc1.my_f" }, +{ "id": "my_h1", "kind": "sink", "where": "parameter1", "taint": "T1", "function": "interproc1.my_h", "message": "There is a T1 flow" } +] diff --git a/regression/goto-analyzer/taint-interproc1/test.desc b/regression/goto-analyzer/taint-interproc1/test.desc new file mode 100644 index 00000000000..1a60e0a17f0 --- /dev/null +++ b/regression/goto-analyzer/taint-interproc1/test.desc @@ -0,0 +1,8 @@ +CORE +interproc1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file interproc1.java line 13( function .*)?: There is a T1 flow \(taint rule my_h1\)$ +-- +^warning: ignoring diff --git a/regression/taint/map1/map1.class b/regression/goto-analyzer/taint-map1/map1.class similarity index 100% rename from regression/taint/map1/map1.class rename to regression/goto-analyzer/taint-map1/map1.class diff --git a/regression/taint/map1/map1.java b/regression/goto-analyzer/taint-map1/map1.java similarity index 100% rename from regression/taint/map1/map1.java rename to regression/goto-analyzer/taint-map1/map1.java diff --git a/regression/taint/map1/taint.json b/regression/goto-analyzer/taint-map1/taint.json similarity index 100% rename from regression/taint/map1/taint.json rename to regression/goto-analyzer/taint-map1/taint.json diff --git a/regression/goto-analyzer/taint-map1/test.desc b/regression/goto-analyzer/taint-map1/test.desc new file mode 100644 index 00000000000..5d7ad41dc91 --- /dev/null +++ b/regression/goto-analyzer/taint-map1/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +map1.class +--taint taint.json +^EXIT=0$ +^SIGNAL=0$ +^file map1.java line 12( function .*)?: There is a flow \(taint rule my_sink\)$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/dump-vararg1/main.c b/regression/goto-instrument/dump-vararg1/main.c new file mode 100644 index 00000000000..9ce2bce8d03 --- /dev/null +++ b/regression/goto-instrument/dump-vararg1/main.c @@ -0,0 +1,19 @@ +#include +#include + +void bb_verror_msg(const char *s, va_list p, const char *strerr) { +} + +void bb_error_msg(const char *s, ...) +{ + va_list p; + va_start(p, s); + bb_verror_msg(s, p, NULL); + va_end(p); +} + +int main() { + bb_error_msg("FOOO"); + return 0; +} + diff --git a/regression/goto-instrument/dump-vararg1/test.desc b/regression/goto-instrument/dump-vararg1/test.desc new file mode 100644 index 00000000000..d1a6d2f2d6f --- /dev/null +++ b/regression/goto-instrument/dump-vararg1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +va_list +-- +^warning: ignoring diff --git a/regression/goto-instrument/print-internal-representation/main.c b/regression/goto-instrument/print-internal-representation/main.c new file mode 100644 index 00000000000..029bfdaa638 --- /dev/null +++ b/regression/goto-instrument/print-internal-representation/main.c @@ -0,0 +1,6 @@ +char stage2_start[100]; + +int main(){ + int x = 3; + unsigned y = 4; +} diff --git a/regression/goto-instrument/print-internal-representation/test.desc b/regression/goto-instrument/print-internal-representation/test.desc new file mode 100644 index 00000000000..d9bbe50625d --- /dev/null +++ b/regression/goto-instrument/print-internal-representation/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--print-internal-representation +^EXIT=0$ +^SIGNAL=0$ +^ \* identifier: __CPROVER_initialize$ +^ \* identifier: main::1::x$ +^ \* identifier: main::1::y$ +-- +-- +Ensures that the output from pretty() is printed when +--print-internal-representation is passed to goto-instrument. diff --git a/regression/goto-instrument/typedef1/main.c b/regression/goto-instrument/typedef1/main.c new file mode 100644 index 00000000000..8c80dc61e34 --- /dev/null +++ b/regression/goto-instrument/typedef1/main.c @@ -0,0 +1,69 @@ +typedef long int off_t; +typedef signed char smallint; + +typedef struct chain_s { + struct node_s *first; + struct node_s *last; + const char *programname; +} chain; + +typedef struct func_s { + struct chain_s body; +} func; + +typedef struct node_s { + struct node_s *n; +} node; + +typedef struct dumper_t_x { + node n; + off_t dump_skip; + signed int dump_length; + smallint dump_vflag; +} dumper_t; + +typedef struct FS_x { + struct FS *nextfs; + signed int bcnt; +} FS; + +dumper_t * alloc_dumper(void) { + return (void*) 0; +} + +typedef unsigned int uint32_t; + +const uint32_t xx[2]; + +typedef struct node_s2 { + uint32_t info; +} node2; + +typedef struct { + int x; +} anon_name; + +typedef struct node_s3 { + union { + struct node_s *n; + func *f; + } r; +} node3; + +typedef int x_int; +typedef int y_int; +typedef x_int *p_int; + +int main() { + node n; + chain c; + dumper_t a; + dumper_t b[3]; + node2* sn; + anon_name d; + node3* s3; + y_int y; + p_int p; + alloc_dumper(); + return 0; +} diff --git a/regression/goto-instrument/typedef1/test.desc b/regression/goto-instrument/typedef1/test.desc new file mode 100644 index 00000000000..8047eddf32b --- /dev/null +++ b/regression/goto-instrument/typedef1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test should be run via chain.sh, which will try to recompile the dumped C +code. Missing/incomplete typedef output would cause a failure. diff --git a/regression/goto-instrument/typedef2/main.c b/regression/goto-instrument/typedef2/main.c new file mode 100644 index 00000000000..928abcfde9a --- /dev/null +++ b/regression/goto-instrument/typedef2/main.c @@ -0,0 +1,16 @@ +typedef struct +{ + char bogus; +} bb_mbstate_t; + +int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps); + +int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps) +{ + return 1; +} + +int main() { + bb_wcrtomb("foo", 'Z', (void*)1); + return 0; +} diff --git a/regression/goto-instrument/typedef2/test.desc b/regression/goto-instrument/typedef2/test.desc new file mode 100644 index 00000000000..8047eddf32b --- /dev/null +++ b/regression/goto-instrument/typedef2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test should be run via chain.sh, which will try to recompile the dumped C +code. Missing/incomplete typedef output would cause a failure. diff --git a/regression/goto-instrument/typedef3/main.c b/regression/goto-instrument/typedef3/main.c new file mode 100644 index 00000000000..4ca41b69451 --- /dev/null +++ b/regression/goto-instrument/typedef3/main.c @@ -0,0 +1,30 @@ +extern void* memset(void *, int, unsigned long); + +typedef void (*__sighandler_t) (int); + +typedef __sighandler_t sighandler_t; + +typedef struct siginfo { + int si_signo; +} siginfo_t; + +struct sigaction { + union { + __sighandler_t _sa_handler; + void (*_sa_sigaction)(int, struct siginfo *, void *); + } _u; +}; + +#define sa_sigaction _u._sa_sigaction +#define sa_handler _u._sa_handler + +static void askpass_timeout(signed int ignore) { + ; +} + +int main() { + struct sigaction sa, oldsa; + memset(&sa, 0, sizeof(sa)); + sa.sa_handler = askpass_timeout; + return 0; +} diff --git a/regression/goto-instrument/typedef3/test.desc b/regression/goto-instrument/typedef3/test.desc new file mode 100644 index 00000000000..8047eddf32b --- /dev/null +++ b/regression/goto-instrument/typedef3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test should be run via chain.sh, which will try to recompile the dumped C +code. Missing/incomplete typedef output would cause a failure. diff --git a/regression/goto-instrument/typedef4/main.c b/regression/goto-instrument/typedef4/main.c new file mode 100644 index 00000000000..7290f9c9ba5 --- /dev/null +++ b/regression/goto-instrument/typedef4/main.c @@ -0,0 +1,23 @@ +#ifndef _WIN32 + +#include +#include + +void sig_block(int sig) +{ + sigset_t ss; + sigemptyset(&ss); + sigaddset(&ss, sig); + sigprocmask(SIG_BLOCK, &ss, NULL); +} + +int main() { + sig_block(0); + return 0; +} +#else +int main() +{ + return 0; +} +#endif diff --git a/regression/goto-instrument/typedef4/test.desc b/regression/goto-instrument/typedef4/test.desc new file mode 100644 index 00000000000..8047eddf32b --- /dev/null +++ b/regression/goto-instrument/typedef4/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dump-c +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test should be run via chain.sh, which will try to recompile the dumped C +code. Missing/incomplete typedef output would cause a failure. diff --git a/regression/taint/Makefile b/regression/taint/Makefile deleted file mode 100644 index 40dbe9c53be..00000000000 --- a/regression/taint/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -default: tests.log - -test: - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer - -tests.log: ../test.pl - @../test.pl -c ../../../src/goto-analyzer/goto-analyzer - -show: - @for dir in *; do \ - if [ -d "$$dir" ]; then \ - vim -o "$$dir/*.java" "$$dir/*.out"; \ - fi; \ - done; - -clean: - find -name '*.out' -execdir $(RM) '{}' \; - find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log diff --git a/regression/taint/aliasing1/test.desc b/regression/taint/aliasing1/test.desc deleted file mode 100644 index a0ac6401d67..00000000000 --- a/regression/taint/aliasing1/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -aliasing1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file aliasing1.java line 10: There is a flow \(taint rule my_sink\)$ --- -^file aliasing1.java line 8: There is a flow \(taint rule my_sink\)$ -^warning: ignoring diff --git a/regression/taint/basic1/test.desc b/regression/taint/basic1/test.desc deleted file mode 100644 index c4384ac9655..00000000000 --- a/regression/taint/basic1/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -basic1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file basic1.java line 8: There is a T1 flow \(taint rule my_h1\)$ -^file basic1.java line 11: There is a T2 flow \(taint rule my_h2\)$ --- -^warning: ignoring diff --git a/regression/taint/basic2/test.desc b/regression/taint/basic2/test.desc deleted file mode 100644 index 428281280c8..00000000000 --- a/regression/taint/basic2/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -basic2.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file basic2.java line 8: There is a T1 flow \(taint rule my_h1\)$ -^file basic2.java line 11: There is a T2 flow \(taint rule my_h2\)$ --- -^warning: ignoring diff --git a/regression/taint/interface1/test.desc b/regression/taint/interface1/test.desc deleted file mode 100644 index 6ac81f15786..00000000000 --- a/regression/taint/interface1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -interface1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file interface1.java line 18: There is a flow! \(taint rule sink_rule\)$ --- -^warning: ignoring diff --git a/regression/taint/map1/test.desc b/regression/taint/map1/test.desc deleted file mode 100644 index 5526aa21b3a..00000000000 --- a/regression/taint/map1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -map1.class ---taint taint.json -^EXIT=0$ -^SIGNAL=0$ -^file map1.java line 12: There is a flow \(taint rule my_sink\)$ --- -^warning: ignoring diff --git a/scripts/cpplint.py b/scripts/cpplint.py index 64fab3758f9..6f8797445ef 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -1967,7 +1967,9 @@ def GetHeaderGuardCPPVariable(filename): fileinfo = FileInfo(filename) file_path_from_root = fileinfo.RepositoryName() - file_path_from_root = 'CPROVER_' + file_path_from_root[4:] + # Remove first path component + offset=len(file_path_from_root.split(os.path.sep)[0])+1 + file_path_from_root = 'CPROVER_' + file_path_from_root[offset:] if _root: suffix = os.sep # On Windows using directory separator will leave us with diff --git a/scripts/ls_parse.py b/scripts/ls_parse.py new file mode 100755 index 00000000000..556b55fa50d --- /dev/null +++ b/scripts/ls_parse.py @@ -0,0 +1,520 @@ +#!/usr/bin/env python3 +# +# Dump info about linker script symbols that pertain to addresses and sizes. +# +# Author: Kareem Khazem +# Copyright Amazon, Inc. 2017 + + +import argparse +import json +import logging +from logging import error, warning, info, debug +import os +import re +import subprocess +import sys +import textwrap + + +def epilog(): + return textwrap.dedent(""" + This script generates a C file containing two kinds of information: + + - The values of symbols that are defined in a linker script; these + are printed as C definitions, like + char *bss_start = (char *)4070047185u; + + - The extent of ELF sections that are defined in a linker script; + these are printed as CPROVER annotations, like + __CPROVER_allocated_memory(0xe9fda44b, 4096); + + A goto-binary of this C file can be linked into the rest of the + codebase that you wish to analyse. This provides CPROVER with + definitions that it otherwise would not have access to, since they + are defined in a linker script rather than C code. This information + can also be printed in JSON rather than as a C file, so that CPROVER + can invoke and use this script without user intervention. + + This script needs a list of symbols declared but never defined in C + code. The hacky way of supplying this list is by passing the path to + the codebase with the --dir flag; this script will scan the codebase + for extern-declared variables. A better way is to generate that list + with CPROVER, and pass that list in using --sym-file. The argument + to --sym-file can be a filename, or '-' for stdin. + """) + + +"""`Running-regex' linker script parser. We don't currently use a full +grammar, as we only need a fraction of the information contained in +linker scripts to give to CBMC. If in the future we need a more +sophisticated parser, we should use an actual grammar from a real +parser. GNU LD uses a YACC/Flex setup and has a very complete grammar, +but we cannot use it (GPL 3). LLD (the LLVM project's linker script +parser) is hand-written (so no explicit grammar), but they do not aim to +support all of GNU LD's syntax, so LLD doesn't work on some real linker +scripts. So in summary: use this regex parser while it's practical; +switch to LLD when needed, and possibly contribute to LLD development to +support parsing your use case.""" +def get_linker_script_data(script): + try: + with open(script) as f: + lines = f.read().splitlines() + except IOError: + error("Linker script '%s' not found", script) + exit(1) + + text = " ".join(lines) + text = re.sub(r"\s+", " ", text) + + # In these regexes, we always start by matching a whitespace. This + # is so that we don't match every substring of an identifier. i.e. + # if we have a section definition .text : { ..., then we only want + # to recognise a section called ".text", and not also "text", "ext", + # "xt", and "t". + # + # Just to be safe, ensure that the first character of the linker + # script is a whitespace. + text = " %s" % text + + close_brace = re.compile(r"\s}") + memory_cmd = re.compile(r"\sMEMORY\s*{") + sections_cmd = re.compile(r"\sSECTIONS\s*{") + assign_current = re.compile(r"\s(?P\w+)\s*=\s*\.\s*;") + sec_def = re.compile(r"\s(?P([-\.\w]+)|(/DISCARD/))" + r"\s+([^:{};]*?):([^:{};])*?{") + assign_size = re.compile(r"\s(?P\w+)\s*=\s*SIZEOF\(" + r"(?P\.\w+)\)\s*;") + memory_block = re.compile(r"\s(?P\w+)\s*:\s*ORIGIN\s*=\s*" + r"(?P0x[a-fA-F0-9]+)\s*,\s*" + r"LENGTH\s*=\s*(?P\d+)\s*" + r"(?P[KMG])") + exp = r"(ORIGIN\(\w+\)|LENGTH\(\w+\))" + op = r"(\+|\-)" + assign_expr = re.compile(r"\s(?P\w+)\s*=\s*" + r"(?P{exp}(\s*{op}\s*{exp})*)" + r"\s*;".format(exp=exp, op=op)) + + # If we match a regex, call the right function to update the state + # with the info gleaned from the matched string. + jump_table = { + close_brace : close_brace_fun, + memory_cmd : memory_cmd_fun, + sections_cmd : sections_cmd_fun, + assign_current : assign_current_fun, + memory_block : memory_block_fun, + sec_def : sec_def_fun, + assign_size : assign_size_fun, + assign_expr : assign_expr_fun, + } + + # Whenever we match an interesting regex, we'll update the state + # with whatever information we want to rip from that bit of text. + state = {} + + # The section definition that we were last in. + state["cur-sec"] = None + + # If we know what section *start* the current address (.) points to, + # then this will not be None. It's used to match an assignment to + # the start of a section. + state["start-valid"] = None + + # If we have just seen an assignment, then this will not be None. + # It's used to match up an assignment with the end of a section. + state["end-valid"] = None + + # Each entry here maps a section name to a map. That map maps "size" + # to the symbol pointing to the size of the section, and "start" + # to the symbol pointing to the start address of the section. One of + # "start" or "size" may be absent, if we couldn't get that bit of + # information from the linker script. + state["sections"] = {} + + # We can use the list of valid addresses to sanity-check that the + # start addresses of sections are genuinely addresses. + state["valid-addresses"] = [] + + # Symbols that get some expression assigned to them, either inside + # or outside a section definition. We'll match them up later. + state["expr-assigns"] = [] + + # These are to sanity-check the parsing. + state["MEM"] = False + state["SEC"] = False + state["DEF"] = False + + i = 0 + while i < len(text): + buf = text[i:] + i += 1 + asrt(not (state["MEM"] and state["SEC"]), + "memory & sections", buf) + asrt(not state["DEF"] or state["SEC"], + "def outside SECTION", buf) + + jump_fun = None + matched_str = None + matched_re = None + match = None + for regex, fun in jump_table.items(): + m = regex.match(buf) + if m: + if jump_fun is not None: + error("matched multiple regexes\n%s", buf) + exit(1) + jump_fun = fun + match = m + matched_str = buf[m.span()[0]:m.span()[1]] + for s, v in locals().items(): + if v is regex and s is not "regex": + matched_re = s + if jump_fun is not None: + info("regex '%s' matched '%s'", matched_re, matched_str) + jump_fun(state, match, buf) + i = i + match.span()[1] - 1 + else: + debug("Clobbering due to '%s'...", buf[:20]) + # There may have been some intermediate command between the + # start of a section definition and where we are. So we have + # no idea what address the current address pointer refers to + state["start-valid"] = None + # There may have been an intermediate command between the + # last assignment and the end of the section. + state["end-valid"] = None + match_up_expr_assigns(state) + return state + + +def assign_expr_fun(state, match, _): + # Do NOT invalidate 'start-valid' here. Assignments from expressions + # do not actually advance the current address pointer. + sym, expr = match.group("sym"), match.group("expr") + origin_pat = r"ORIGIN\((?P\w+?)\)" + origins = re.findall(origin_pat, expr) + if len(origins) != 1: + info("assign with %d origins, skipping: %s", len(origins), + match.string()) + return + ret = {"origin": origins[0], "sym": sym} + for block_name, data in state["blocks"].items(): + for op in ["ORIGIN", "LENGTH"]: + old_expr = str(expr) + expr = re.sub(r"%s\(%s\)" % (op, block_name), str(data[op]), + expr) + if expr != old_expr: + info("Subbed %s(%s) with %d", op, block_name, data[op]) + info("Final expression is '%s'. Evaluating; " + "may the angels have mercy on my soul.", expr) + try: + ret["addr"] = eval(expr) + except RuntimeError: + warning("Unable to evaluate '%s'" , expr) + info("Evaluated '%s' to %d", expr, ret["addr"]) + state["expr-assigns"].append(ret) + + +def sec_def_fun(state, match, buf): + asrt(not state["DEF"], "nested sec def", buf) + state["DEF"] = True + sec = match.group("sec") + info("Current section is now '%s'", sec) + state["cur-sec"] = sec + state["start-valid"] = True + + +def assign_size_fun(state, match, buf): + asrt(state["SEC"], "assignment outside SECTIONS", buf) + sec = match.group("sec") + if sec not in state["sections"]: + state["sections"][sec] = {} + sym = match.group("sym") + info("'%s' marks the size of section '%s'", sym, sec) + state["sections"][sec]["size"] = sym + + +def assign_current_fun(state, match, buf): + asrt(state["SEC"], "assignment outside SECTIONS", buf) + sec = state["cur-sec"] + state["end-valid"] = match + if state["start-valid"]: + if sec not in state["sections"]: + state["sections"][sec] = {} + sym = match.group("sym") + info("'%s' marks the start of section '%s'", sym, sec) + state["sections"][sec]["start"] = sym + else: + info("Don't know where we are.") + + +def close_brace_fun(state, _, buf): + # We might have seen an assignment immediately before this. + if state["end-valid"]: + asrt(state["DEF"], "end-valid outside sec-def", buf) + sec = state["cur-sec"] + if sec in state["sections"]: + sym = state["end-valid"].group("sym") + info("'%s' marks the end of section '%s'", sym, sec) + state["sections"][sec]["end"] = sym + else: + # Linker script assigned end-of-section to a symbol, but not + # the start. this is useless to us. + pass + + if state["DEF"]: + info("Closing sec-def") + state["DEF"] = False + elif state["SEC"]: + info("Closing sections") + state["SEC"] = False + elif state["MEM"]: + info("Closing memory command") + state["MEM"] = False + else: + error("Not in block\n%s", buf) + exit(1) + + +def memory_block_fun(state, m, buf): + asrt(state["MEM"], "memory block outside MEMORY", buf) + start, length, unit = m.group("orig"), m.group("len"), m.group("unit") + length = int(length) + dec_start = int(start, 16) + mul = {"K": 1000, "M": 1000000, "G": 1000000000} + length = length * mul[unit] + end = dec_start + length + info("mem block %s from %d to %d (%d%s long)", start, dec_start, end, + length, unit) + state["valid-addresses"].append({"from": dec_start, "to": end}) + + name = m.group("name") + if "blocks" not in state: + state["blocks"] = {} + state["blocks"][name] = {"ORIGIN": int(start, 16), "LENGTH": length} + + +def sections_cmd_fun(state, _, buf): + asrt(not state["SEC"], "encountered SECTIONS twice", buf) + state["SEC"] = True + + +def memory_cmd_fun(state, _, buf): + asrt(not state["MEM"], "encountered MEMORY twice", buf) + state["MEM"] = True + + +def match_up_expr_assigns(state): + blocks = set([data["origin"] for data in state["expr-assigns"]]) + for block in blocks: + assigns = [a for a in state["expr-assigns"] + if a["origin"] == block] + assigns = sorted(assigns, key=(lambda a: a["addr"])) + if len(assigns) < 2: + warning("Only 1 assignment to expr involving %s", block) + continue + start_addr, end_addr = assigns[0]["addr"], assigns[-1]["addr"] + start_sym, end_sym = assigns[0]["sym"], assigns[-1]["sym"] + info("Valid memory from %s (%d) to %s (%s) [%s block]", + start_sym, start_addr, end_sym, end_addr, block) + tmp = {"start": start_sym, "end": end_sym} + sec_name = "BLOCK_%s_%s-%s" % (block, start_sym, end_sym) + state["sections"][sec_name] = tmp + + +def asrt(cond, msg, buf): + if not cond: + error("%s\n%s", msg, buf) + exit(1) + + +def needed_definitions(all_symbols, root_dir): + ret = [] + pat = re.compile(r"extern\s+char\s+(?P\w+)\[\];") + allowed = [".c", ".cpp", ".h"] + for root, _, files in os.walk(root_dir): + for file in files: + file = os.path.join(root, file) + _, ext = os.path.splitext(file) + if ext not in allowed: + continue + with open(file) as f: + for line in f: + m = pat.match(line) + if m: + ret.append(m.group("var")) + bad = [v for v in ret if v not in all_symbols] + if bad: + logging.error("These symbols need definitions but are not " + "in the object file: %s", ", ".join(bad)) + exit(1) + logging.info("need symbols:\n%s", "\n".join(ret)) + return ret + + +def symbols_from(object_file): + cmd = ["objdump", "--syms", object_file] + proc = subprocess.Popen(cmd, universal_newlines=True, + stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + if proc.wait(): + logging.error("`%s` failed. Output:\n%s", " ".join(cmd), + proc.stdout.read()) + exit(1) + pat = re.compile(r"(?P[^\s]+)\s+" + r"(?P[lgu! ][w ][C ][W ][Ii ][Dd ][FfO ])\s+" + r"(?P
[^\s]+)\s+" + r"(?P[0-9a-f]+)\s+" + r"(?P[^\s]*)" # Can be empty! + ) + matching = False + ret = {} + for line in proc.stdout.read().splitlines(): + if not line: + continue + if not matching and re.match("SYMBOL TABLE:", line): + matching = True + continue + if not matching: + continue + m = pat.match(line) + if not m: + logging.error("Unexpected line from `%s`:\n%s", + " ".join(cmd), line) + exit(1) + ret[m.group("name")] = m.group("addr") + logging.info("found symbols:\n%s", "\n".join( + ["0x%-16s %s" % (v, k) for k, v in ret.items()])) + return ret + + +def match_up_addresses(script_data, symbol_table): + ret = [] + for data in script_data["sections"].values(): + ok = False + if "size" in data and "start" in data: + ok = True + if "end" in data and "start" in data: + ok = True + if not ok: + continue + region = {} + for sym, value in symbol_table.items(): + if "size" in data and sym == data["size"]: + region["size"] = {"sym": sym, "val": value} + if "start" in data and sym == data["start"]: + region["start"] = {"sym": sym, "val": value} + if "end" in data and sym == data["end"]: + region["end"] = {"sym": sym, "val": value} + append = False + if "size" in region and "start" in region: + append = True + if "end" in region and "start" in region: + append = True + if append: + ret.append(region) + return ret + + +def get_region_range(region): + ret = {} + if "end" in region: + start = int(region["start"]["val"], 16) + end = int(region["end"]["val"], 16) + size = end - start + s_var = region["start"]["sym"] + e_var = region["end"]["sym"] + ret["start"] = start + ret["size"] = size + ret["annot"] = "__CPROVER_allocated_memory(%s, %d);" % (hex(start), size) + ret["commt"] = "from %s to %s" % (s_var, e_var) + elif "size" in region: + start = int(region["start"]["val"], 16) + size = int(region["size"]["val"], 16) + s_var = region["start"]["sym"] + z_var = region["size"]["sym"] + ret["start"] = start + ret["size"] = size + ret["annot"] = "__CPROVER_allocated_memory(%s, %d);" % (hex(start), size) + ret["commt"] = "from %s for %s bytes" % (s_var, z_var) + else: + raise "Malformatted region\n%s" % str(region) + return ret + + +def final_json_output(regions, symbol_table): + ret = {"regions": [], "addresses": []} + for s, v in symbol_table.items(): + ret["addresses"].append({"sym": s, "val": int(v, 16)}) + for region in regions: + ret["regions"].append(get_region_range(region)) + return ret + + + +def symbols_from_file(sym_file): + if sym_file == "-": + return [s.strip() for s in sys.stdin.readlines()] + else: + with open(sym_file) as f: + return [s.strip() for s in f.readlines()] + + +def main(): + pars = argparse.ArgumentParser( + description="Generate info about linker-defined symbols and regions.", + epilog=epilog(), + formatter_class=argparse.RawDescriptionHelpFormatter) + pars.add_argument("-s", "--script", metavar="S", required=True, + help="path to linker script") + pars.add_argument("-o", "--object", metavar="O", required=True, + help="path to fully-linked binary") + + sym_source = pars.add_mutually_exclusive_group(required=True) + sym_source.add_argument("-d", "--dir", metavar="D", + help="path to top-level of codebase") + sym_source.add_argument("-i", "--sym-file", + metavar="F", help="file of names of linker symbols") + + pars.add_argument("-t", "--out-file", metavar="F", + help="default: stdout", default=None) + + verbs = pars.add_mutually_exclusive_group() + verbs.add_argument("-v", "--verbose", action="store_true") + verbs.add_argument("-w", "--very-verbose", action="store_true") + + args = pars.parse_args() + + if args.verbose: + lvl = logging.INFO + elif args.very_verbose: + lvl = logging.DEBUG + else: + lvl = logging.WARNING + form = "linkerscript parse %(levelname)s: %(message)s" + logging.basicConfig(format=form, level=lvl) + + script_data = get_linker_script_data(args.script) + symbol_table = symbols_from(args.object) + if args.dir: + needed = needed_definitions(symbol_table.keys(), args.dir) + else: + needed = symbols_from_file(args.sym_file) + symbol_table = {k:v for k, v in symbol_table.items() if k in needed} + + regions = match_up_addresses(script_data, symbol_table) + + info(json.dumps(symbol_table, indent=2)) + info(json.dumps(script_data, indent=2)) + info(json.dumps(regions, indent=2)) + + final = json.dumps(final_json_output(regions, symbol_table), + indent=2) + if args.out_file: + with open(args.out_file, "w") as f: + f.write(final) + info(final) + else: + print(final) + + +if __name__ == "__main__": + main() diff --git a/scripts/reformat_docs.py b/scripts/reformat_docs.py index 35dc6e12809..eadc5359052 100644 --- a/scripts/reformat_docs.py +++ b/scripts/reformat_docs.py @@ -95,6 +95,10 @@ def is_block_valid(self, block): def convert_sections(self, block): return [self.format_module(block)] + def needs_new_header(self, file_contents): + return (re.search(r'^\/\/\/ \\file$', file_contents, flags=re.MULTILINE) + is None) + class FunctionFormatter(GenericFormatter): def __init__(self, doc_width): @@ -188,6 +192,7 @@ def convert_sections(self, block): def replace_block( block_contents, + file_contents, file, header_formatter, class_formatter, @@ -199,9 +204,10 @@ def replace_block( {f.name: f.contents for f in parse_fields(block_contents.group(1))}) if header_formatter.is_block_valid(block): - return '%s%s\n' % ( - block_contents.group(0), - header_formatter.convert(header_from_block(block))) + converted = header_formatter.convert(header_from_block(block)) + if header_formatter.needs_new_header(file_contents) and converted: + return block_contents.group(0) + converted + '\n' + return block_contents.group(0) if class_formatter.is_block_valid(block): return class_formatter.convert(class_from_block(block)) @@ -231,6 +237,7 @@ def convert_file(file, inplace): new_contents = block_re.sub( lambda match: replace_block( match, + contents, file, header_formatter, class_formatter, diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index face9d8ae67..fd64d085850 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -210,9 +210,6 @@ void custom_bitvector_domaint::transform( ai_baset &ai, const namespacet &ns) { - if(has_values.is_false()) - return; - // upcast of ai custom_bitvector_analysist &cba= static_cast(ai); @@ -337,6 +334,54 @@ void custom_bitvector_domaint::transform( } } } + else + { + goto_programt::const_targett next=from; + ++next; + + // only if there is an actual call, i.e., we have a body + if(next!=to) + { + const code_typet &code_type= + to_code_type(ns.lookup(identifier).type); + + code_function_callt::argumentst::const_iterator arg_it= + code_function_call.arguments().begin(); + for(const auto ¶m : code_type.parameters()) + { + const irep_idt &p_identifier=param.get_identifier(); + if(p_identifier.empty()) + continue; + + // there may be a mismatch in the number of arguments + if(arg_it==code_function_call.arguments().end()) + break; + + // assignments arguments -> parameters + symbol_exprt p=ns.lookup(p_identifier).symbol_expr(); + // may alias other stuff + std::set lhs_set=cba.aliases(p, from); + + vectorst rhs_vectors=get_rhs(*arg_it); + + for(const auto &lhs : lhs_set) + { + assign_lhs(lhs, rhs_vectors); + } + + // is it a pointer? + if(p.type().id()==ID_pointer) + { + dereference_exprt lhs_deref(p); + dereference_exprt rhs_deref(*arg_it); + vectorst rhs_vectors=get_rhs(rhs_deref); + assign_lhs(lhs_deref, rhs_vectors); + } + + ++arg_it; + } + } + } } } break; @@ -484,44 +529,55 @@ bool custom_bitvector_domaint::merge( locationt from, locationt to) { - if(b.has_values.is_false()) - return false; // no change - - if(has_values.is_false()) - { - *this=b; - return true; // change - } - - bool changed=false; + bool changed=has_values.is_false(); + has_values=tvt::unknown(); // first do MAY - for(const auto &bit : may_bits) + bitst::iterator it=may_bits.begin(); + for(const auto &bit : b.may_bits) { - bit_vectort &a_bits=may_bits[bit.first]; - bit_vectort old=a_bits; - a_bits|=bit.second; - if(old!=a_bits) + while(it!=may_bits.end() && it->firstfirst) + { + may_bits.insert(it, bit); changed=true; + } + else if(it!=may_bits.end()) + { + bit_vectort &a_bits=it->second; + bit_vectort old=a_bits; + a_bits|=bit.second; + if(old!=a_bits) + changed=true; + + ++it; + } } // now do MUST - for(auto &bit : must_bits) + it=must_bits.begin(); + for(auto &bit : b.must_bits) { - bitst::const_iterator b_it= - b.must_bits.find(bit.first); - - if(b_it==b.must_bits.end()) + while(it!=must_bits.end() && it->firstfirst) { - bit_vectort old=bit.second; - bit.second&=bit.second; - if(old!=bit.second) + must_bits.insert(it, bit); + changed=true; + } + else if(it!=must_bits.end()) + { + bit_vectort &a_bits=it->second; + bit_vectort old=a_bits; + a_bits&=bit.second; + if(old!=a_bits) changed=true; + + ++it; } } diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index ff2884cc2ec..5ef03adbaf2 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -87,7 +87,7 @@ class custom_bitvector_domaint:public ai_domain_baset tvt has_values; - custom_bitvector_domaint():has_values(true) + custom_bitvector_domaint():has_values(false) { } @@ -145,6 +145,7 @@ class custom_bitvector_analysist:public ait protected: virtual void initialize(const goto_functionst &_goto_functions) { + ait::initialize(_goto_functions); local_may_alias_factory(_goto_functions); } diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 3076442a3ee..d078324679f 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -18,8 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "ai.h" #include "interval_template.h" -typedef interval_template integer_intervalt; -typedef interval_template ieee_float_intervalt; +typedef interval_templatet integer_intervalt; +typedef interval_templatet ieee_float_intervalt; class interval_domaint:public ai_domain_baset { diff --git a/src/analyses/interval_template.h b/src/analyses/interval_template.h index b06013af53e..eeeb5f32653 100644 --- a/src/analyses/interval_template.h +++ b/src/analyses/interval_template.h @@ -15,15 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com #include -template class interval_template +template class interval_templatet { public: - interval_template():lower_set(false), upper_set(false) + interval_templatet():lower_set(false), upper_set(false) { // this is 'top' } - explicit interval_template(const T &x): + explicit interval_templatet(const T &x): lower_set(true), upper_set(true), lower(x), @@ -31,7 +31,7 @@ template class interval_template { } - explicit interval_template(const T &l, const T &u): + explicit interval_templatet(const T &l, const T &u): lower_set(true), upper_set(true), lower(l), @@ -102,18 +102,18 @@ template class interval_template } // Union or disjunction - void join(const interval_template &i) + void join(const interval_templatet &i) { approx_union_with(i); } // Intersection or conjunction - void meet(const interval_template &i) + void meet(const interval_templatet &i) { intersect_with(i); } - void intersect_with(const interval_template &i) + void intersect_with(const interval_templatet &i) { if(i.lower_set) { @@ -142,7 +142,7 @@ template class interval_template } } - void approx_union_with(const interval_template &i) + void approx_union_with(const interval_templatet &i) { if(i.lower_set && lower_set) lower=std::min(lower, i.lower); @@ -157,7 +157,7 @@ template class interval_template }; template -tvt operator<=(const interval_template &a, const interval_template &b) +tvt operator<=(const interval_templatet &a, const interval_templatet &b) { if(a.upper_set && b.lower_set && a.upper<=b.lower) return tvt(true); @@ -168,25 +168,25 @@ tvt operator<=(const interval_template &a, const interval_template &b) } template -tvt operator>=(const interval_template &a, const interval_template &b) +tvt operator>=(const interval_templatet &a, const interval_templatet &b) { return b<=a; } template -tvt operator<(const interval_template &a, const interval_template &b) +tvt operator<(const interval_templatet &a, const interval_templatet &b) { return !(a>=b); } template -tvt operator>(const interval_template &a, const interval_template &b) +tvt operator>(const interval_templatet &a, const interval_templatet &b) { return !(a<=b); } template -bool operator==(const interval_template &a, const interval_template &b) +bool operator==(const interval_templatet &a, const interval_templatet &b) { if(a.lower_set!=b.lower_set) return false; @@ -202,31 +202,31 @@ bool operator==(const interval_template &a, const interval_template &b) } template -bool operator!=(const interval_template &a, const interval_template &b) +bool operator!=(const interval_templatet &a, const interval_templatet &b) { return !(a==b); } template -interval_template upper_interval(const T &u) +interval_templatet upper_interval(const T &u) { - interval_template i; + interval_templatet i; i.upper_set=true; i.upper=u; return i; } template -interval_template lower_interval(const T &l) +interval_templatet lower_interval(const T &l) { - interval_template i; + interval_templatet i; i.lower_set=true; i.lower=l; return i; } template -std::ostream &operator << (std::ostream &out, const interval_template &i) +std::ostream &operator << (std::ostream &out, const interval_templatet &i) { if(i.lower_set) out << '[' << i.lower; diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index 6def40f54a8..b9ee53e45dd 100644 --- a/src/analyses/invariant_set.h +++ b/src/analyses/invariant_set.h @@ -88,7 +88,7 @@ class invariant_sett ineq_sett ne_set; // bounds - typedef interval_template boundst; + typedef interval_templatet boundst; typedef std::map bounds_mapt; bounds_mapt bounds_map; diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index a29419961a0..1468b5441b6 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -197,6 +197,18 @@ void ansi_c_internal_additions(std::string &code) "long double __CPROVER_infl(void);\n" "int __CPROVER_thread_local __CPROVER_rounding_mode="+ std::to_string(config.ansi_c.rounding_mode)+";\n" + "int __CPROVER_isgreaterf(float f, float g);\n" + "int __CPROVER_isgreaterd(double f, double g);\n" + "int __CPROVER_isgreaterequalf(float f, float g);\n" + "int __CPROVER_isgreaterequald(double f, double g);\n" + "int __CPROVER_islessf(float f, float g);\n" + "int __CPROVER_islessd(double f, double g);\n" + "int __CPROVER_islessequalf(float f, float g);\n" + "int __CPROVER_islessequald(double f, double g);\n" + "int __CPROVER_islessgreaterf(float f, float g);\n" + "int __CPROVER_islessgreaterd(double f, double g);\n" + "int __CPROVER_isunorderedf(float f, float g);\n" + "int __CPROVER_isunorderedd(double f, double g);\n" // absolute value "int __CPROVER_abs(int x);\n" diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 185c576e401..4b84899fc1a 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2566,7 +2566,7 @@ exprt c_typecheck_baset::do_special_functions( // http://gcc.gnu.org/onlinedocs/gcc-4.1.1/gcc/Atomic-Builtins.html // adjust return type of function to match pointer subtype - if(expr.arguments().size()<1) + if(expr.arguments().empty()) { err_location(f_op); error() << "__sync_* primitives take as least one argument" << eom; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 4f18ea3db29..972febbff3a 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -570,6 +570,14 @@ std::string expr2ct::convert_rec( c_qualifierst ret_qualifiers; ret_qualifiers.read(code_type.return_type()); + // _Noreturn should go with the return type + if(new_qualifiers.is_noreturn) + { + ret_qualifiers.is_noreturn=true; + new_qualifiers.is_noreturn=false; + q=new_qualifiers.as_string(); + } + const typet &return_type=code_type.return_type(); // return type may be a function pointer or array @@ -1845,10 +1853,12 @@ std::string expr2ct::convert_constant( if(dest!="" && isdigit(dest[dest.size()-1])) { + if(dest.find('.')==std::string::npos) + dest+=".0"; + + // ANSI-C: double is default; float/long-double require annotation if(src.type()==float_type()) dest+='f'; - else if(src.type()==double_type()) - dest+=""; // ANSI-C: double is default else if(src.type()==long_double_type()) dest+='l'; } @@ -2600,7 +2610,7 @@ std::string expr2ct::convert_code_switch( const codet &src, unsigned indent) { - if(src.operands().size()<1) + if(src.operands().empty()) { unsigned precedence; return convert_norep(src, precedence); @@ -3534,7 +3544,11 @@ std::string expr2ct::convert_with_precedence( return convert_function(src, "isinf", precedence=16); else if(src.id()==ID_bswap) - return convert_function(src, "bswap", precedence=16); + return convert_function( + src, + "__builtin_bswap"+ + integer2string(pointer_offset_bits(src.op0().type(), ns)), + precedence=16); else if(src.id()==ID_isnormal) return convert_function(src, "isnormal", precedence=16); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index ac9c529145a..251bb828b6f 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -92,6 +92,7 @@ double __CPROVER_inf(void); float __CPROVER_inff(void); long double __CPROVER_infl(void); //extern int __CPROVER_thread_local __CPROVER_rounding_mode; +int __CPROVER_isgreaterd(double f, double g); // absolute value int __CPROVER_abs(int); diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 7312708fb8c..1af12148d83 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -22,8 +22,69 @@ inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); } inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); } +/* FUNCTION: __CPROVER_isgreaterf */ + +int __CPROVER_isgreaterf(float f, float g) { return f > g; } + +/* FUNCTION: __CPROVER_isgreaterd */ + +int __CPROVER_isgreaterd(double f, double g) { return f > g; } + +/* FUNCTION: __CPROVER_isgreaterequalf */ + +int __CPROVER_isgreaterequalf(float f, float g) { return f >= g; } + +/* FUNCTION: __CPROVER_isgreaterequald */ + +int __CPROVER_isgreaterequald(double f, double g) { return f >= g; } + +/* FUNCTION: __CPROVER_islessf */ + +int __CPROVER_islessf(float f, float g) { return f < g;} + +/* FUNCTION: __CPROVER_islessd */ + +int __CPROVER_islessd(double f, double g) { return f < g;} + +/* FUNCTION: __CPROVER_islessequalf */ + +int __CPROVER_islessequalf(float f, float g) { return f <= g; } + +/* FUNCTION: __CPROVER_islessequald */ + +int __CPROVER_islessequald(double f, double g) { return f <= g; } + +/* FUNCTION: __CPROVER_islessgreaterf */ + +int __CPROVER_islessgreaterf(float f, float g) { return (f < g) || (f > g); } + +/* FUNCTION: __CPROVER_islessgreaterd */ + +int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); } + +/* FUNCTION: __CPROVER_isunorderedf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); } + +/* FUNCTION: __CPROVER_isunorderedd */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); } + + /* FUNCTION: isfinite */ +#undef isfinite + int isfinite(double d) { return __CPROVER_isfinited(d); } /* FUNCTION: __finite */ @@ -40,6 +101,8 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); } /* FUNCTION: isinf */ +#undef isinf + inline int isinf(double d) { return __CPROVER_isinfd(d); } /* FUNCTION: __isinf */ @@ -64,6 +127,8 @@ inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); } /* FUNCTION: isnan */ +#undef isnan + inline int isnan(double d) { return __CPROVER_isnand(d); } /* FUNCTION: __isnan */ @@ -88,6 +153,8 @@ inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); } /* FUNCTION: isnormal */ +#undef isnormal + inline int isnormal(double d) { return __CPROVER_isnormald(d); } /* FUNCTION: __isnormalf */ @@ -152,6 +219,8 @@ inline int _fdsign(float f) { return __CPROVER_signf(f); } /* FUNCTION: signbit */ +#undef signbit + inline int signbit(double d) { return __CPROVER_signd(d); } /* FUNCTION: __signbitd */ @@ -423,10 +492,70 @@ float __builtin_nanf(const char *str) { // the 'str' argument is not yet used __CPROVER_hide:; + (void)*str; + return 0.0f/0.0f; +} + + +/* ISO 9899:2011 + * The call nan("n-char-sequence") is equivalent to + * strtod("NAN(n-char-sequence)", (char**) NULL); the call nan("") is + * equivalent to strtod("NAN()", (char**) NULL). If tagp does not + * point to an n-char sequence or an empty string, the call is + * equivalent to strtod("NAN", (char**) NULL). Calls to nanf and nanl + * are equivalent to the corresponding calls to strtof and strtold. + * + * The nan functions return a quiet NaN, if available, with content + * indicated through tagp. If the implementation does not support + * quiet NaNs, the functions return zero. + */ + +/* FUNCTION: nan */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +double nan(const char *str) { + // the 'str' argument is not yet used + __CPROVER_hide:; + (void)*str; + return 0.0/0.0; +} + +/* FUNCTION: nanf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +float nanf(const char *str) { + // the 'str' argument is not yet used + __CPROVER_hide:; + (void)*str; + return 0.0f/0.0f; +} + +/* FUNCTION: nanl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +long double nanl(const char *str) { + // the 'str' argument is not yet used + __CPROVER_hide:; (void)*str; return 0.0/0.0; } + + + + /* FUNCTION: nextUpf */ #ifndef __CPROVER_LIMITS_H_INCLUDED @@ -575,6 +704,7 @@ __CPROVER_hide:; --m.bv; return m.f; } + } @@ -608,8 +738,6 @@ __CPROVER_hide:; float nextUpf(float f); -extern int __CPROVER_rounding_mode; - float sqrtf(float f) { __CPROVER_hide:; @@ -645,7 +773,7 @@ float sqrtf(float f) __CPROVER_assume(f < upperSquare); // Select between them to work out which to return - switch(__CPROVER_rounding_mode) + switch(fegetround()) { case FE_TONEAREST : return (f - lowerSquare < upperSquare - f) ? lower : upper; break; @@ -720,7 +848,7 @@ double sqrt(double d) __CPROVER_assume(lowerSquare <= d); __CPROVER_assume(d < upperSquare); - switch(__CPROVER_rounding_mode) + switch(fegetround()) { case FE_TONEAREST: return (d - lowerSquare < upperSquare - d) ? lower : upper; break; @@ -789,7 +917,7 @@ long double sqrtl(long double d) __CPROVER_assume(lowerSquare <= d); __CPROVER_assume(d < upperSquare); - switch(__CPROVER_rounding_mode) + switch(fegetround()) { case FE_TONEAREST: return (d - lowerSquare < upperSquare - d) ? lower : upper; break; @@ -816,3 +944,1381 @@ long double sqrtl(long double d) return root; } } + + +/* ISO 9899:2011 + * The fmax functions determine the maximum numeric value of their + * arguments. 242) + * + * 242) NaN arguments are treated as missing data: if one argument is + * a NaN and the other numeric, then the fmax functions choose the + * numeric value. See F.10.9.2. + * + * - If just one argument is a NaN, the fmax functions return the other + * argument (if both arguments are NaNs, the functions return a NaN). + * - The returned value is exact and is independent of the current + * rounding direction mode. + * - The body of the fmax function might be 374) + * { return (isgreaterequal(x, y) || isnan(y)) ? x : y; } + * + * 374) Ideally, fmax would be sensitive to the sign of zero, for + * example fmax(-0.0, +0.0) would return +0; however, implementation + * in software might be impractical. + */ + +/* FUNCTION: fmax */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +double fmax(double f, double g) { return ((f >= g) || isnan(g)) ? f : g; } + +/* FUNCTION : fmaxf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +float fmaxf(float f, float g) { return ((f >= g) || isnan(g)) ? f : g; } + + +/* FUNCTION : fmaxl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +long double fmaxl(long double f, long double g) { return ((f >= g) || isnan(g)) ? f : g; } + + +/* ISO 9899:2011 + * The fmin functions determine the minimum numeric value of their + * arguments.243) + * + * 243) The fmin functions are analogous to the fmax functions in + * their treatment of NaNs. + * + * - The fmin functions are analogous to the fmax functions (see F.10.9.2). + * - The returned value is exact and is independent of the current + * rounding direction mode. + */ + +/* FUNCTION: fmin */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +double fmin(double f, double g) { return ((f <= g) || isnan(g)) ? f : g; } + +/* FUNCTION: fminf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +float fminf(float f, float g) { return ((f <= g) || isnan(g)) ? f : g; } + +/* FUNCTION: fminl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +// TODO : Should call a __CPROVER_function so that it can be converted to SMT-LIB +long double fminl(long double f, long double g) { return ((f <= g) || isnan(g)) ? f : g; } + + +/* ISO 9899:2011 + * The fdim functions determine the positive difference between their + * arguments: + * x - y if x > y + * +0 if x <= y + * A range error may occur. + */ + +/* FUNCTION: fdim */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +double fdim(double f, double g) { return ((f > g) ? f - g : +0.0); } + + +/* FUNCTION: fdimf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); } + + +/* FUNCTION: fdiml */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); } + + + +/* FUNCTION: __sort_of_CPROVER_round_to_integral */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d) +{ + double magicConst = 0x1.0p+52; + double return_value; + int saved_rounding_mode = fegetround(); + fesetround(rounding_mode); + + if (fabs(d) >= magicConst || d == 0.0) + { + return_value = d; + } + else + { + if (!signbit(d)) { + double tmp = d + magicConst; + return_value = tmp - magicConst; + } else { + double tmp = d - magicConst; + return_value = tmp + magicConst; + } + } + + fesetround(saved_rounding_mode); + return return_value; +} + +/* FUNCTION: __sort_of_CPROVER_round_to_integralf */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d) +{ + float magicConst = 0x1.0p+23f; // 23 is significant + float return_value; + int saved_rounding_mode = fegetround(); + fesetround(rounding_mode); + + if (fabsf(d) >= magicConst || d == 0.0) + { + return_value = d; + } + else + { + if (!signbit(d)) { + float tmp = d + magicConst; + return_value = tmp - magicConst; + } else { + float tmp = d - magicConst; + return_value = tmp + magicConst; + } + } + + fesetround(saved_rounding_mode); + return return_value; +} + + +/* FUNCTION: __sort_of_CPROVER_round_to_integrall */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d) +{ + long double magicConst = 0x1.0p+64; + long double return_value; + int saved_rounding_mode = fegetround(); + fesetround(rounding_mode); + + if (fabsl(d) >= magicConst || d == 0.0) + { + return_value = d; + } + else + { + if (!signbit(d)) { + long double tmp = d + magicConst; + return_value = tmp - magicConst; + } else { + long double tmp = d - magicConst; + return_value = tmp + magicConst; + } + } + + fesetround(saved_rounding_mode); + return return_value; +} + +/* ISO 9899:2011 + * + * The ceil functions compute the smallest integer value not less than + * x. + */ + +/* FUNCTION: ceil */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double ceil(double x) +{ + return __sort_of_CPROVER_round_to_integral(FE_UPWARD, x); +} + +/* FUNCTION: ceilf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float ceilf(float x) +{ + return __sort_of_CPROVER_round_to_integralf(FE_UPWARD, x); +} + + +/* FUNCTION: ceill */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double ceill(long double x) +{ + return __sort_of_CPROVER_round_to_integrall(FE_UPWARD, x); +} + + +/* ISO 9899:2011 + * + * The floor functions compute the largest integer value not greater than x. + */ + +/* FUNCTION: floor */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double floor(double x) +{ + return __sort_of_CPROVER_round_to_integral(FE_DOWNWARD, x); +} + +/* FUNCTION: floorf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float floorf(float x) +{ + return __sort_of_CPROVER_round_to_integralf(FE_DOWNWARD, x); +} + + +/* FUNCTION: floorl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double floorl(long double x) +{ + return __sort_of_CPROVER_round_to_integrall(FE_DOWNWARD, x); +} + + +/* ISO 9899:2011 + * + * The trunc functions round their argument to the integer value, in + * floating format, nearest to but no larger in magnitude than the argument. + */ + +/* FUNCTION: trunc */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double trunc(double x) +{ + return __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, x); +} + +/* FUNCTION: truncf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float truncf(float x) +{ + return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x); +} + + +/* FUNCTION: truncl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double truncl(long double x) +{ + return __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, x); +} + + +/* ISO 9899:2011 + * + * The round functions round their argument to the integer value, in + * floating format, nearest to but no larger in magnitude than the argument. + */ + +/* FUNCTION: round */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double round(double x) +{ + // Tempting but RNE not RNA + // return __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x); + + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + return __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp); +} + +/* FUNCTION: roundf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float roundf(float x) +{ + // Tempting but RNE not RNA + // return __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x); + + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + float xp; + if (x > 0.0f) { + xp = x + 0.5f; + } else if (x < 0.0f) { + xp = x - 0.5f; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp); +} + + +/* FUNCTION: roundl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double roundl(long double x) +{ + // Tempting but RNE not RNA + // return __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x); + + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + long double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + return __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp); +} + + + +/* ISO 9899:2011 + * + * The nearbyint functions round their argument to an integer value in + * floating-point format, using the current rounding direction and + * without raising the inexact floating-point exception. + */ + +/* FUNCTION: nearbyint */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double nearbyint(double x) +{ + return __sort_of_CPROVER_round_to_integral(fegetround(), x); +} + +/* FUNCTION: nearbyintf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float nearbyintf(float x) +{ + return __sort_of_CPROVER_round_to_integralf(fegetround(), x); +} + + +/* FUNCTION: nearbyintl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double nearbyintl(long double x) +{ + return __sort_of_CPROVER_round_to_integrall(fegetround(), x); +} + + + +/* ISO 9899:2011 + * + * The rint functions differ from the nearbyint functions (7.12.9.3) + * only in that the rint functions may raise the inexact + * floating-point exception if the result differs in value from the argument. + */ + +/* FUNCTION: rint */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double rint(double x) +{ + return __sort_of_CPROVER_round_to_integral(fegetround(), x); +} + +/* FUNCTION: rintf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float rintf(float x) +{ + return __sort_of_CPROVER_round_to_integralf(fegetround(), x); +} + +/* FUNCTION: rintl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double rintl(long double x) +{ + return __sort_of_CPROVER_round_to_integrall(fegetround(), x); +} + + + +/* ISO 9899:2011 + * + * The lrint and llrint functions round their argument to the nearest + * integer value, rounding according to the current rounding + * direction. If the rounded value is outside the range of the return + * type, the numeric result is unspecified and a domain error or range + * error may occur. + */ + +/* FUNCTION: lrint */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +long int lrint(double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + double rti = __sort_of_CPROVER_round_to_integral(fegetround(), x); + return (long int)rti; +} + +/* FUNCTION: lrintf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +long int lrintf(float x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + float rti = __sort_of_CPROVER_round_to_integralf(fegetround(), x); + return (long int)rti; +} + + +/* FUNCTION: lrintl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long int lrintl(long double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + long double rti = __sort_of_CPROVER_round_to_integrall(fegetround(), x); + return (long int)rti; +} + + +/* FUNCTION: llrint */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +long long int llrint(double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + double rti = __sort_of_CPROVER_round_to_integral(fegetround(), x); + return (long long int)rti; +} + +/* FUNCTION: llrintf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +long long int llrintf(float x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + float rti = __sort_of_CPROVER_round_to_integralf(fegetround(), x); + return (long long int)rti; +} + + +/* FUNCTION: llrintl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long long int llrintl(long double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT + long double rti = __sort_of_CPROVER_round_to_integrall(fegetround(), x); + return (long long int)rti; +} + + +/* ISO 9899:2011 + * + * The lround and llround functions round their argument to the + * nearest integer value, rounding halfway cases away from zero, + * regardless of the current rounding direction. If the rounded value + * is outside the range of the return type, the numeric result is + * unspecified and a domain error or range error may occur. + */ + +/* FUNCTION: lround */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +long int lround(double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp); + return (long int)rti; +} + +/* FUNCTION: lroundf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +long int lroundf(float x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + float xp; + if (x > 0.0f) { + xp = x + 0.5f; + } else if (x < 0.0f) { + xp = x - 0.5f; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp); + return (long int)rti; +} + + +/* FUNCTION: lroundl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long int lroundl(long double x) +{ + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + long double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp); + return (long int)rti; +} + + +/* FUNCTION: llround */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +long long int llround(double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp); + return (long long int)rti; +} + +/* FUNCTION: llroundf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +long long int llroundf(float x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + float xp; + if (x > 0.0f) { + xp = x + 0.5f; + } else if (x < 0.0f) { + xp = x - 0.5f; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp); + return (long long int)rti; +} + + +/* FUNCTION: llroundl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long long int llroundl(long double x) +{ + // TODO : should be an all-in-one __CPROVER function to allow + // conversion to SMT, plus should use RNA + int saved_rounding_mode = fegetround(); + fesetround(FE_TOWARDZERO); + + long double xp; + if (x > 0.0) { + xp = x + 0.5; + } else if (x < 0.0) { + xp = x - 0.5; + } else { + xp = x; + } + + fesetround(saved_rounding_mode); + + long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp); + return (long long int)rti; +} + + +/* ISO 9899:2011 + * + * The modf functions break the argument value into integral and + * fractional parts, each of which has the same type and sign as the + * argument. They store the integral part (in floating-point format) + * in the object pointed to by iptr. + */ + +/* FUNCTION: modf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double modf(double x, double *iptr) +{ + *iptr = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, x); + return (x - *iptr); +} + +/* FUNCTION: modff */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + + float modff(float x, float *iptr) +{ + *iptr = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x); + return (x - *iptr); +} + + +/* FUNCTION: modfl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + + long double modfl(long double x, long double *iptr) +{ + *iptr = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, x); + return (x - *iptr); +} + + + +/* FUNCTION: __sort_of_CPROVER_remainder */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB +double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d); + +double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y) +{ + if (x == 0.0 || __CPROVER_isinfd(y)) + return x; + + // Extended precision helps... a bit... + long double div = x/y; + long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); + long double res = (-y * n) + x; // TODO : FMA would be an improvement + return res; +} + +/* FUNCTION: __sort_of_CPROVER_remainderf */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB + +float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d); + +float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y) +{ + if (x == 0.0f || __CPROVER_isinff(y)) + return x; + + // Extended precision helps... a bit... + long double div = x/y; + long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); + long double res = (-y * n) + x; // TODO : FMA would be an improvement + return res; +} + +/* FUNCTION: __sort_of_CPROVER_remainderl */ +// TODO : Should be a real __CPROVER function to convert to SMT-LIB + +long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d); + +long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y) +{ + if (x == 0.0 || __CPROVER_isinfld(y)) + return x; + + // Extended precision helps... a bit... + long double div = x/y; + long double n = __sort_of_CPROVER_round_to_integral(rounding_mode,div); + long double res = (-y * n) + x; // TODO : FMA would be an improvement + return res; +} + + + +/* ISO 9899:2011 + * + * The fmod functions return the value x - ny, for some + * integer n such that, if y is nonzero, the result has the same sign + * as x and magnitude less than the magnitude of y. If y is zero, + * whether a domain error occurs or the fmod functions return zero is + * implementation-defined. + */ + +/* FUNCTION: fmod */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y); + +double fmod(double x, double y) { return __sort_of_CPROVER_remainder(FE_TOWARDZERO, x, y); } + + +/* FUNCTION: fmodf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y); + +float fmodf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TOWARDZERO, x, y); } + + +/* FUNCTION: fmodl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y); + +long double fmodl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TOWARDZERO, x, y); } + + + +/* ISO 9899:2011 + * + * The remainder functions compute the remainder x REM y required by + * IEC 60559.239) + * + * 239) "When y != 0, the remainder r = x REM y is defined regardless + * of the rounding mode by the mathematical relation r = x - n + * y, where n is the integer nearest the exact value of x/y; + * whenever | n - x/y | = 1/2, then n is even. If r = 0, its + * sign shall be that of x." This definition is applicable for + * all implementations. + */ + +/* FUNCTION: remainder */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +double __sort_of_CPROVER_remainder (int rounding_mode, double x, double y); + +double remainder(double x, double y) { return __sort_of_CPROVER_remainder(FE_TONEAREST, x, y); } + + +/* FUNCTION: remainderf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +float __sort_of_CPROVER_remainderf (int rounding_mode, float x, float y); + +float remainderf(float x, float y) { return __sort_of_CPROVER_remainderf(FE_TONEAREST, x, y); } + + +/* FUNCTION: remainderl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +#ifndef __CPROVER_FENV_H_INCLUDED +#include +#define __CPROVER_FENV_H_INCLUDED +#endif + +long double __sort_of_CPROVER_remainderl (int rounding_mode, long double x, long double y); + +long double remainderl(long double x, long double y) { return __sort_of_CPROVER_remainderl(FE_TONEAREST, x, y); } + + + + +/* ISO 9899:2011 + * The copysign functions produce a value with the magnitude of x and + * the sign of y. They produce a NaN (with the sign of y) if x is a + * NaN. On implementations that represent a signed zero but do not + * treat negative zero consistently in arithmetic operations, the + * copysign functions regard the sign of zero as positive. + */ + +/* FUNCTION: copysign */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +double fabs (double d); + +double copysign(double x, double y) +{ + double abs = fabs(x); + return (signbit(y)) ? -abs : abs; +} + +/* FUNCTION: copysignf */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +float fabsf (float d); + +float copysignf(float x, float y) +{ + float abs = fabs(x); + return (signbit(y)) ? -abs : abs; +} + +/* FUNCTION: copysignl */ + +#ifndef __CPROVER_MATH_H_INCLUDED +#include +#define __CPROVER_MATH_H_INCLUDED +#endif + +long double fabsl (long double d); + +long double copysignl(long double x, long double y) +{ + long double abs = fabs(x); + return (signbit(y)) ? -abs : abs; +} + + + diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 42aadee4326..6537445e88b 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -146,7 +146,7 @@ int clobber_parse_optionst::doit() if(!out) throw std::string("failed to create file simulator.c"); - dump_c(goto_functions, true, ns, out); + dump_c(goto_functions, true, false, ns, out); status() << "instrumentation complete; compile and execute simulator.c" << eom; @@ -192,7 +192,7 @@ bool clobber_parse_optionst::get_goto_program( const optionst &options, goto_functionst &goto_functions) { - if(cmdline.args.size()==0) + if(cmdline.args.empty()) { error() << "Please provide a program to verify" << eom; return true; diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 6e2cce31d74..bb0b207e699 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -466,7 +466,7 @@ void cpp_typecheckt::typecheck_compound_declarator( { is_virtual=true; const code_typet &code_type=to_code_type(comp.type()); - assert(code_type.parameters().size()>0); + assert(!code_type.parameters().empty()); const typet &pointer_type=code_type.parameters()[0].type(); assert(pointer_type.id()==ID_pointer); virtual_bases.insert(pointer_type.subtype().get(ID_identifier)); diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 1e33634ebef..cc357d1fb21 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -574,13 +574,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( expr.type().subtype().id()==ID_code) { code_typet code1=to_code_type(expr.type().subtype()); - assert(code1.parameters().size()>0); + assert(!code1.parameters().empty()); code_typet::parametert this1=code1.parameters()[0]; assert(this1.get(ID_C_base_name)==ID_this); code1.parameters().erase(code1.parameters().begin()); code_typet code2=to_code_type(type.subtype()); - assert(code2.parameters().size()>0); + assert(!code2.parameters().empty()); code_typet::parametert this2=code2.parameters()[0]; assert(this2.get(ID_C_base_name)==ID_this); code2.parameters().erase(code2.parameters().begin()); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 979572c717e..e2926f09607 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1431,7 +1431,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name( // http://gcc.gnu.org/onlinedocs/gcc-4.1.1/gcc/Atomic-Builtins.html // adjust return type of function to match pointer subtype - if(fargs.operands.size()<1) + if(fargs.operands.empty()) { error().source_location=source_location; error() << "__sync_* primitives take as least one argument" diff --git a/src/doxyfile b/src/doxyfile index 611614a3a9b..7d894c4e704 100644 --- a/src/doxyfile +++ b/src/doxyfile @@ -1,96 +1,129 @@ -# Doxyfile 1.5.6 +# Doxyfile 1.8.11 # This file describes the settings to be used by the documentation system -# doxygen (www.doxygen.org) for a project +# doxygen (www.doxygen.org) for a project. # -# All text after a hash (#) is considered a comment and will be ignored +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. # The format is: -# TAG = value [value, ...] -# For lists items can also be appended using: -# TAG += value [value, ...] -# Values that contain spaces should be placed between quotes (" ") +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). #--------------------------------------------------------------------------- # Project related configuration options #--------------------------------------------------------------------------- # This tag specifies the encoding used for all characters in the config file -# that follow. The default is UTF-8 which is also the encoding used for all -# text before the first occurrence of this tag. Doxygen uses libiconv (or the -# iconv built into libc) for the transcoding. See -# http://www.gnu.org/software/libiconv for the list of possible encodings. +# that follow. The default is UTF-8 which is also the encoding used for all text +# before the first occurrence of this tag. Doxygen uses libiconv (or the iconv +# built into libc) for the transcoding. See http://www.gnu.org/software/libiconv +# for the list of possible encodings. +# The default value is: UTF-8. DOXYFILE_ENCODING = UTF-8 -# The PROJECT_NAME tag is a single word (or a sequence of words surrounded -# by quotes) that should identify the project. +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. PROJECT_NAME = cprover -# The PROJECT_NUMBER tag can be used to enter a project or revision number. -# This could be handy for archiving the generated documentation or -# if some version control system is used. +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. + +PROJECT_NUMBER = + +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. -PROJECT_NUMBER = +PROJECT_BRIEF = -# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) -# base path where the generated documentation will be put. -# If a relative path is entered, it will be relative to the location -# where doxygen was started. If left blank the current directory will be used. +# With the PROJECT_LOGO tag one can specify a logo or an icon that is included +# in the documentation. The maximum height of the logo should not exceed 55 +# pixels and the maximum width should not exceed 200 pixels. Doxygen will copy +# the logo to the output directory. + +PROJECT_LOGO = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. OUTPUT_DIRECTORY = ../doc -# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create -# 4096 sub-directories (in 2 levels) under the output directory of each output -# format and will distribute the generated files over these directories. -# Enabling this option can be useful when feeding doxygen a huge amount of -# source files, where putting all generated files in the same directory would -# otherwise cause performance problems for the file system. +# If the CREATE_SUBDIRS tag is set to YES then doxygen will create 4096 sub- +# directories (in 2 levels) under the output directory of each output format and +# will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. +# The default value is: NO. CREATE_SUBDIRS = NO +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + # The OUTPUT_LANGUAGE tag is used to specify the language in which all # documentation generated by doxygen is written. Doxygen will use this # information to generate all constant output in the proper language. -# The default language is English, other supported languages are: -# Afrikaans, Arabic, Brazilian, Catalan, Chinese, Chinese-Traditional, -# Croatian, Czech, Danish, Dutch, Farsi, Finnish, French, German, Greek, -# Hungarian, Italian, Japanese, Japanese-en (Japanese with English messages), -# Korean, Korean-en, Lithuanian, Norwegian, Macedonian, Persian, Polish, -# Portuguese, Romanian, Russian, Serbian, Slovak, Slovene, Spanish, Swedish, -# and Ukrainian. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese, +# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States), +# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian, +# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages), +# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian, +# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian, +# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish, +# Ukrainian and Vietnamese. +# The default value is: English. OUTPUT_LANGUAGE = English -# If the BRIEF_MEMBER_DESC tag is set to YES (the default) Doxygen will -# include brief member descriptions after the members that are listed in -# the file and class documentation (similar to JavaDoc). -# Set to NO to disable this. +# If the BRIEF_MEMBER_DESC tag is set to YES, doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. BRIEF_MEMBER_DESC = YES -# If the REPEAT_BRIEF tag is set to YES (the default) Doxygen will prepend -# the brief description of a member or function before the detailed description. -# Note: if both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# If the REPEAT_BRIEF tag is set to YES, doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the # brief descriptions will be completely suppressed. +# The default value is: YES. REPEAT_BRIEF = YES -# This tag implements a quasi-intelligent brief description abbreviator -# that is used to form the text in various listings. Each string -# in this list, if found as the leading text of the brief description, will be -# stripped from the text and the result after processing the whole list, is -# used as the annotated text. Otherwise, the brief description is used as-is. -# If left blank, the following values are used ("$name" is automatically -# replaced with the name of the entity): "The $name class" "The $name widget" -# "The $name file" "is" "provides" "specifies" "contains" -# "represents" "a" "an" "the" +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. -ABBREVIATE_BRIEF = +ABBREVIATE_BRIEF = # If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then -# Doxygen will generate a detailed section even if there is only a brief +# doxygen will generate a detailed section even if there is only a brief # description. +# The default value is: NO. ALWAYS_DETAILED_SEC = NO @@ -98,1123 +131,1984 @@ ALWAYS_DETAILED_SEC = NO # inherited members of a class in the documentation of that class as if those # members were ordinary class members. Constructors, destructors and assignment # operators of the base classes will not be shown. +# The default value is: NO. INLINE_INHERITED_MEMB = NO -# If the FULL_PATH_NAMES tag is set to YES then Doxygen will prepend the full -# path before files name in the file list and in the header files. If set -# to NO the shortest path that makes the file name unique will be used. +# If the FULL_PATH_NAMES tag is set to YES, doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. FULL_PATH_NAMES = YES -# If the FULL_PATH_NAMES tag is set to YES then the STRIP_FROM_PATH tag -# can be used to strip a user-defined part of the path. Stripping is -# only done if one of the specified strings matches the left-hand part of -# the path. The tag can be used to show relative paths in the file list. -# If left blank the directory from which doxygen is run is used as the -# path to strip. +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. -STRIP_FROM_PATH = +STRIP_FROM_PATH = -# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of -# the path mentioned in the documentation of a class, which tells -# the reader which header file to include in order to use a class. -# If left blank only the name of the header file containing the class -# definition is used. Otherwise one should specify the include paths that -# are normally passed to the compiler using the -I flag. +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. -STRIP_FROM_INC_PATH = +STRIP_FROM_INC_PATH = -# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter -# (but less readable) file names. This can be useful is your file systems -# doesn't support long names like on DOS, Mac, or CD-ROM. +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. SHORT_NAMES = NO -# If the JAVADOC_AUTOBRIEF tag is set to YES then Doxygen -# will interpret the first line (until the first dot) of a JavaDoc-style -# comment as the brief description. If set to NO, the JavaDoc -# comments will behave just like regular Qt-style comments -# (thus requiring an explicit @brief command for a brief description.) +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. JAVADOC_AUTOBRIEF = YES -# If the QT_AUTOBRIEF tag is set to YES then Doxygen will -# interpret the first line (until the first dot) of a Qt-style -# comment as the brief description. If set to NO, the comments -# will behave just like regular Qt-style comments (thus requiring -# an explicit \brief command for a brief description.) +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. QT_AUTOBRIEF = NO -# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make Doxygen -# treat a multi-line C++ special comment block (i.e. a block of //! or /// -# comments) as a brief description. This used to be the default behaviour. -# The new default is to treat a multi-line C++ comment block as a detailed -# description. Set this tag to YES if you prefer the old behaviour instead. +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. MULTILINE_CPP_IS_BRIEF = NO -# If the DETAILS_AT_TOP tag is set to YES then Doxygen -# will output the detailed description near the top, like JavaDoc. -# If set to NO, the detailed description appears after the member -# documentation. - -DETAILS_AT_TOP = YES - -# If the INHERIT_DOCS tag is set to YES (the default) then an undocumented -# member inherits the documentation from any documented member that it -# re-implements. +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. INHERIT_DOCS = YES -# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce -# a new page for each member. If set to NO, the documentation of a member will -# be part of the file/class/namespace that contains it. +# If the SEPARATE_MEMBER_PAGES tag is set to YES then doxygen will produce a new +# page for each member. If set to NO, the documentation of a member will be part +# of the file/class/namespace that contains it. +# The default value is: NO. SEPARATE_MEMBER_PAGES = NO -# The TAB_SIZE tag can be used to set the number of spaces in a tab. -# Doxygen uses this value to replace tabs by spaces in code fragments. +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. TAB_SIZE = 8 -# This tag can be used to specify a number of aliases that acts -# as commands in the documentation. An alias has the form "name=value". -# For example adding "sideeffect=\par Side Effects:\n" will allow you to -# put the command \sideeffect (or @sideeffect) in the documentation, which -# will result in a user-defined paragraph with heading "Side Effects:". -# You can put \n's in the value part of an alias to insert newlines. +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:\n" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". You can put \n's in the value part of an alias to insert +# newlines. -ALIASES = +ALIASES = -# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C -# sources only. Doxygen will then generate output that is more tailored for C. -# For instance, some of the names that are used will be different. The list -# of all members will be omitted, etc. +# This tag can be used to specify a number of word-keyword mappings (TCL only). +# A mapping has the form "name=value". For example adding "class=itcl::class" +# will allow you to use the command class in the itcl::class meaning. + +TCL_SUBST = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. OPTIMIZE_OUTPUT_FOR_C = NO -# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java -# sources only. Doxygen will then generate output that is more tailored for -# Java. For instance, namespaces will be presented as packages, qualified -# scopes will look different, etc. +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. OPTIMIZE_OUTPUT_JAVA = NO # Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran -# sources only. Doxygen will then generate output that is more tailored for -# Fortran. +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. OPTIMIZE_FOR_FORTRAN = NO # Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL -# sources. Doxygen will then generate output that is tailored for -# VHDL. +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. OPTIMIZE_OUTPUT_VHDL = NO +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, Javascript, +# C#, C, C++, D, PHP, Objective-C, Python, Fortran (fixed format Fortran: +# FortranFixed, free formatted Fortran: FortranFree, unknown formatted Fortran: +# Fortran. In the later case the parser tries to guess whether the code is fixed +# or free formatted code, this is the default for Fortran type files), VHDL. For +# instance to make doxygen treat .inc files as Fortran files (default is PHP), +# and .f files as C (default is Fortran), use: inc=Fortran f=C. +# +# Note: For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. + +EXTENSION_MAPPING = + +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See http://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. + +MARKDOWN_SUPPORT = YES + +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by putting a % sign in front of the word or +# globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. + +AUTOLINK_SUPPORT = YES + # If you use STL classes (i.e. std::string, std::vector, etc.) but do not want -# to include (a tag file for) the STL sources as input, then you should -# set this tag to YES in order to let doxygen match functions declarations and -# definitions whose arguments contain STL classes (e.g. func(std::string); v.s. -# func(std::string) {}). This also make the inheritance and collaboration +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration # diagrams that involve STL classes more complete and accurate. +# The default value is: NO. BUILTIN_STL_SUPPORT = YES # If you use Microsoft's C++/CLI language, you should set this option to YES to # enable parsing support. +# The default value is: NO. CPP_CLI_SUPPORT = NO -# Set the SIP_SUPPORT tag to YES if your project consists of sip sources only. -# Doxygen will parse them like normal C++ but will assume all classes use public -# instead of private inheritance when no explicit protection keyword is present. +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# http://www.riverbankcomputing.co.uk/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. SIP_SUPPORT = NO -# For Microsoft's IDL there are propget and propput attributes to indicate getter -# and setter methods for a property. Setting this option to YES (the default) -# will make doxygen to replace the get and set methods by a property in the -# documentation. This will only work if the methods are indeed getting or -# setting a simple type. If this is not the case, or you want to show the -# methods anyway, you should set this option to NO. +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. IDL_PROPERTY_SUPPORT = YES # If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC -# tag is set to YES, then doxygen will reuse the documentation of the first +# tag is set to YES then doxygen will reuse the documentation of the first # member in the group (if any) for the other members of the group. By default # all members of a group must be documented explicitly. +# The default value is: NO. DISTRIBUTE_GROUP_DOC = NO -# Set the SUBGROUPING tag to YES (the default) to allow class member groups of -# the same type (for instance a group of public functions) to be put as a -# subgroup of that type (e.g. under the Public Functions section). Set it to -# NO to prevent subgrouping. Alternatively, this can be done per class using -# the \nosubgrouping command. +# If one adds a struct or class to a group and this option is enabled, then also +# any nested class or struct is added to the same group. By default this option +# is disabled and one has to add nested compounds explicitly via \ingroup. +# The default value is: NO. + +GROUP_NESTED_COMPOUNDS = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. SUBGROUPING = YES -# When TYPEDEF_HIDES_STRUCT is enabled, a typedef of a struct, union, or enum -# is documented as struct, union, or enum with the name of the typedef. So +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. + +INLINE_GROUPED_CLASSES = NO + +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. + +INLINE_SIMPLE_STRUCTS = NO + +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So # typedef struct TypeS {} TypeT, will appear in the documentation as a struct # with name TypeT. When disabled the typedef will appear as a member of a file, -# namespace, or class. And the struct will be named TypeS. This can typically -# be useful for C code in case the coding convention dictates that all compound +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound # types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. TYPEDEF_HIDES_STRUCT = NO +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. + +LOOKUP_CACHE_SIZE = 0 + #--------------------------------------------------------------------------- # Build related configuration options #--------------------------------------------------------------------------- -# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in -# documentation are documented, even if no documentation was available. -# Private class members and static file members will be hidden unless -# the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES +# If the EXTRACT_ALL tag is set to YES, doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. EXTRACT_ALL = YES -# If the EXTRACT_PRIVATE tag is set to YES all private members of a class -# will be included in the documentation. +# If the EXTRACT_PRIVATE tag is set to YES, all private members of a class will +# be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIVATE = YES -EXTRACT_PRIVATE = NO +# If the EXTRACT_PACKAGE tag is set to YES, all members with package or internal +# scope will be included in the documentation. +# The default value is: NO. -# If the EXTRACT_STATIC tag is set to YES all static members of a file -# will be included in the documentation. +EXTRACT_PACKAGE = NO -EXTRACT_STATIC = NO +# If the EXTRACT_STATIC tag is set to YES, all static members of a file will be +# included in the documentation. +# The default value is: NO. -# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) -# defined locally in source files will be included in the documentation. -# If set to NO only classes defined in header files are included. +EXTRACT_STATIC = YES + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES, classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO, +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. EXTRACT_LOCAL_CLASSES = YES -# This flag is only useful for Objective-C code. When set to YES local -# methods, which are defined in the implementation section but not in -# the interface are included in the documentation. -# If set to NO (the default) only methods in the interface are included. +# This flag is only useful for Objective-C code. If set to YES, local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO, only methods in the interface are +# included. +# The default value is: NO. EXTRACT_LOCAL_METHODS = NO # If this flag is set to YES, the members of anonymous namespaces will be # extracted and appear in the documentation as a namespace called -# 'anonymous_namespace{file}', where file will be replaced with the base -# name of the file that contains the anonymous namespace. By default -# anonymous namespace are hidden. +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. EXTRACT_ANON_NSPACES = NO -# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all -# undocumented members of documented classes, files or namespaces. -# If set to NO (the default) these members will be included in the -# various overviews, but no documentation section is generated. -# This option has no effect if EXTRACT_ALL is enabled. +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. HIDE_UNDOC_MEMBERS = NO -# If the HIDE_UNDOC_CLASSES tag is set to YES, Doxygen will hide all -# undocumented classes that are normally visible in the class hierarchy. -# If set to NO (the default) these classes will be included in the various -# overviews. This option has no effect if EXTRACT_ALL is enabled. +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO, these classes will be included in the various overviews. This option +# has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. HIDE_UNDOC_CLASSES = NO -# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, Doxygen will hide all -# friend (class|struct|union) declarations. -# If set to NO (the default) these declarations will be included in the -# documentation. +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# (class|struct|union) declarations. If set to NO, these declarations will be +# included in the documentation. +# The default value is: NO. HIDE_FRIEND_COMPOUNDS = NO -# If the HIDE_IN_BODY_DOCS tag is set to YES, Doxygen will hide any -# documentation blocks found inside the body of a function. -# If set to NO (the default) these blocks will be appended to the -# function's detailed documentation block. +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO, these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. HIDE_IN_BODY_DOCS = NO -# The INTERNAL_DOCS tag determines if documentation -# that is typed after a \internal command is included. If the tag is set -# to NO (the default) then the documentation will be excluded. -# Set it to YES to include the internal documentation. +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. INTERNAL_DOCS = NO -# If the CASE_SENSE_NAMES tag is set to NO then Doxygen will only generate -# file names in lower-case letters. If set to YES upper-case letters are also +# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file +# names in lower-case letters. If set to YES, upper-case letters are also # allowed. This is useful if you have classes or files whose names only differ # in case and if your file system supports case sensitive file names. Windows # and Mac users are advised to set this option to NO. +# The default value is: system dependent. CASE_SENSE_NAMES = NO -# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen -# will show members with their full class and namespace scopes in the -# documentation. If set to YES the scope will be hidden. +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES, the +# scope will be hidden. +# The default value is: NO. HIDE_SCOPE_NAMES = NO -# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen -# will put a list of the files that are included by a file in the documentation -# of that file. +# If the HIDE_COMPOUND_REFERENCE tag is set to NO (default) then doxygen will +# append additional text to a page's title, such as Class Reference. If set to +# YES the compound reference will be hidden. +# The default value is: NO. + +HIDE_COMPOUND_REFERENCE= NO + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. SHOW_INCLUDE_FILES = YES -# If the INLINE_INFO tag is set to YES (the default) then a tag [inline] -# is inserted in the documentation for inline members. +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. + +FORCE_LOCAL_INCLUDES = NO + +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. INLINE_INFO = YES -# If the SORT_MEMBER_DOCS tag is set to YES (the default) then doxygen -# will sort the (detailed) documentation of file and class members -# alphabetically by member name. If set to NO the members will appear in -# declaration order. +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. +# The default value is: YES. SORT_MEMBER_DOCS = YES -# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the -# brief documentation of file, namespace and class members alphabetically -# by member name. If set to NO (the default) the members will appear in -# declaration order. +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. SORT_BRIEF_DOCS = NO -# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the -# hierarchy of group names into alphabetical order. If set to NO (the default) -# the group names will appear in their defined order. +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. SORT_GROUP_NAMES = NO -# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be -# sorted by fully-qualified names, including namespaces. If set to -# NO (the default), the class list will be sorted only by class name, -# not including the namespace part. +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. # Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. -# Note: This option applies only to the class list, not to the -# alphabetical list. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. SORT_BY_SCOPE_NAME = NO -# The GENERATE_TODOLIST tag can be used to enable (YES) or -# disable (NO) the todo list. This list is created by putting \todo -# commands in the documentation. +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. + +STRICT_PROTO_MATCHING = NO + +# The GENERATE_TODOLIST tag can be used to enable (YES) or disable (NO) the todo +# list. This list is created by putting \todo commands in the documentation. +# The default value is: YES. GENERATE_TODOLIST = YES -# The GENERATE_TESTLIST tag can be used to enable (YES) or -# disable (NO) the test list. This list is created by putting \test -# commands in the documentation. +# The GENERATE_TESTLIST tag can be used to enable (YES) or disable (NO) the test +# list. This list is created by putting \test commands in the documentation. +# The default value is: YES. GENERATE_TESTLIST = YES -# The GENERATE_BUGLIST tag can be used to enable (YES) or -# disable (NO) the bug list. This list is created by putting \bug -# commands in the documentation. +# The GENERATE_BUGLIST tag can be used to enable (YES) or disable (NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. GENERATE_BUGLIST = YES -# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or -# disable (NO) the deprecated list. This list is created by putting -# \deprecated commands in the documentation. +# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or disable (NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. GENERATE_DEPRECATEDLIST= YES -# The ENABLED_SECTIONS tag can be used to enable conditional -# documentation sections, marked by \if sectionname ... \endif. +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. -ENABLED_SECTIONS = +ENABLED_SECTIONS = -# The MAX_INITIALIZER_LINES tag determines the maximum number of lines -# the initial value of a variable or define consists of for it to appear in -# the documentation. If the initializer consists of more lines than specified -# here it will be hidden. Use a value of 0 to hide initializers completely. -# The appearance of the initializer of individual variables and defines in the -# documentation can be controlled using \showinitializer or \hideinitializer -# command in the documentation regardless of this setting. +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. MAX_INITIALIZER_LINES = 30 -# Set the SHOW_USED_FILES tag to NO to disable the list of files generated -# at the bottom of the documentation of classes and structs. If set to YES the +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES, the # list will mention the files that were used to generate the documentation. +# The default value is: YES. SHOW_USED_FILES = YES -# If the sources in your project are distributed over multiple directories -# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy -# in the documentation. The default is NO. - -SHOW_DIRECTORIES = NO - -# Set the SHOW_FILES tag to NO to disable the generation of the Files page. -# This will remove the Files entry from the Quick Index and from the -# Folder Tree View (if specified). The default is YES. +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. SHOW_FILES = YES -# Set the SHOW_NAMESPACES tag to NO to disable the generation of the -# Namespaces page. This will remove the Namespaces entry from the Quick Index -# and from the Folder Tree View (if specified). The default is YES. +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. SHOW_NAMESPACES = YES # The FILE_VERSION_FILTER tag can be used to specify a program or script that # doxygen should invoke to get the current version for each file (typically from # the version control system). Doxygen will invoke the program by executing (via -# popen()) the command , where is the value of -# the FILE_VERSION_FILTER tag, and is the name of an input file -# provided by doxygen. Whatever the program writes to standard output -# is used as the file version. See the manual for examples. +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. + +LAYOUT_FILE = + +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also http://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. See also \cite for info how to create references. -FILE_VERSION_FILTER = +CITE_BIB_FILES = #--------------------------------------------------------------------------- -# configuration options related to warning and progress messages +# Configuration options related to warning and progress messages #--------------------------------------------------------------------------- -# The QUIET tag can be used to turn on/off the messages that are generated -# by doxygen. Possible values are YES and NO. If left blank NO is used. +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. QUIET = YES # The WARNINGS tag can be used to turn on/off the warning messages that are -# generated by doxygen. Possible values are YES and NO. If left blank -# NO is used. +# generated to standard error (stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. WARNINGS = YES -# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings -# for undocumented members. If EXTRACT_ALL is set to YES then this flag will -# automatically be disabled. +# If the WARN_IF_UNDOCUMENTED tag is set to YES then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. WARN_IF_UNDOCUMENTED = YES -# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for -# potential errors in the documentation, such as not documenting some -# parameters in a documented function, or documenting parameters that -# don't exist or using markup commands wrongly. +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some parameters +# in a documented function, or documenting parameters that don't exist or using +# markup commands wrongly. +# The default value is: YES. WARN_IF_DOC_ERROR = YES -# This WARN_NO_PARAMDOC option can be abled to get warnings for -# functions that are documented, but have no documentation for their parameters -# or return value. If set to NO (the default) doxygen will only warn about -# wrong or incomplete parameter documentation, but not about the absence of -# documentation. +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO, doxygen will only warn about wrong or incomplete +# parameter documentation, but not about the absence of documentation. +# The default value is: NO. WARN_NO_PARAMDOC = NO -# The WARN_FORMAT tag determines the format of the warning messages that -# doxygen can produce. The string should contain the $file, $line, and $text -# tags, which will be replaced by the file and line number from which the -# warning originated and the warning text. Optionally the format may contain -# $version, which will be replaced by the version of the file (if it could -# be obtained via FILE_VERSION_FILTER) +# If the WARN_AS_ERROR tag is set to YES then doxygen will immediately stop when +# a warning is encountered. +# The default value is: NO. + +WARN_AS_ERROR = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# The default value is: $file:$line: $text. WARN_FORMAT = "$file:$line: $text" -# The WARN_LOGFILE tag can be used to specify a file to which warning -# and error messages should be written. If left blank the output is written -# to stderr. +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). -WARN_LOGFILE = +WARN_LOGFILE = #--------------------------------------------------------------------------- -# configuration options related to the input files +# Configuration options related to the input files #--------------------------------------------------------------------------- -# The INPUT tag can be used to specify the files and/or directories that contain -# documented source files. You may enter file names like "myfile.cpp" or -# directories like "/usr/src/myproject". Separate the files or directories -# with spaces. +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. See also FILE_PATTERNS and EXTENSION_MAPPING +# Note: If this tag is empty the current directory is searched. INPUT = . # This tag can be used to specify the character encoding of the source files -# that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is -# also the default input encoding. Doxygen uses libiconv (or the iconv built -# into libc) for the transcoding. See http://www.gnu.org/software/libiconv for -# the list of possible encodings. +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: http://www.gnu.org/software/libiconv) for the list of +# possible encodings. +# The default value is: UTF-8. INPUT_ENCODING = UTF-8 # If the value of the INPUT tag contains directories, you can use the -# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp -# and *.h) to filter out the source-files in the directories. If left -# blank the following patterns are tested: -# *.c *.cc *.cxx *.cpp *.c++ *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh *.hxx -# *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.py *.f90 +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# read by doxygen. +# +# If left blank the following patterns are tested:*.c, *.cc, *.cxx, *.cpp, +# *.c++, *.java, *.ii, *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, +# *.hh, *.hxx, *.hpp, *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, +# *.m, *.markdown, *.md, *.mm, *.dox, *.py, *.pyw, *.f90, *.f, *.for, *.tcl, +# *.vhd, *.vhdl, *.ucf, *.qsf, *.as and *.js. -FILE_PATTERNS = *.cpp *.h +FILE_PATTERNS = *.cpp \ + *.h -# The RECURSIVE tag can be used to turn specify whether or not subdirectories -# should be searched for input files as well. Possible values are YES and NO. -# If left blank NO is used. +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. RECURSIVE = YES -# The EXCLUDE tag can be used to specify files and/or directories that should +# The EXCLUDE tag can be used to specify files and/or directories that should be # excluded from the INPUT source files. This way you can easily exclude a # subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is +# run. EXCLUDE = solvers/z3/ -# The EXCLUDE_SYMLINKS tag can be used select whether or not files or -# directories that are symbolic links (a Unix filesystem feature) are excluded +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded # from the input. +# The default value is: NO. EXCLUDE_SYMLINKS = NO # If the value of the INPUT tag contains directories, you can use the # EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude -# certain files from those directories. Note that the wildcards are matched -# against the file with absolute path, so to exclude all test directories -# for example use the pattern */test/* +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* -EXCLUDE_PATTERNS = */.svn/* */.git/* +EXCLUDE_PATTERNS = */.svn/* \ + */.git/* # The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names # (namespaces, classes, functions, etc.) that should be excluded from the # output. The symbol name can be a fully qualified name, a word, or if the # wildcard * is used, a substring. Examples: ANamespace, AClass, # AClass::ANamespace, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* -EXCLUDE_SYMBOLS = +EXCLUDE_SYMBOLS = -# The EXAMPLE_PATH tag can be used to specify one or more files or -# directories that contain example code fragments that are included (see -# the \include command). +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). -EXAMPLE_PATH = +EXAMPLE_PATH = # If the value of the EXAMPLE_PATH tag contains directories, you can use the -# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp -# and *.h) to filter out the source-files in the directories. If left -# blank all files are included. +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. -EXAMPLE_PATTERNS = +EXAMPLE_PATTERNS = # If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be -# searched for input files to be used with the \include or \dontinclude -# commands irrespective of the value of the RECURSIVE tag. -# Possible values are YES and NO. If left blank NO is used. +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. EXAMPLE_RECURSIVE = NO -# The IMAGE_PATH tag can be used to specify one or more files or -# directories that contain image that are included in the documentation (see -# the \image command). +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). -IMAGE_PATH = +IMAGE_PATH = # The INPUT_FILTER tag can be used to specify a program that doxygen should # invoke to filter for each input file. Doxygen will invoke the filter program -# by executing (via popen()) the command , where -# is the value of the INPUT_FILTER tag, and is the name of an -# input file. Doxygen will then use the output that the filter program writes -# to standard output. If FILTER_PATTERNS is specified, this tag will be -# ignored. +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. -INPUT_FILTER = +INPUT_FILTER = # The FILTER_PATTERNS tag can be used to specify filters on a per file pattern -# basis. Doxygen will compare the file name with each pattern and apply the -# filter if there is a match. The filters are a list of the form: -# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further -# info on how filters are used. If FILTER_PATTERNS is empty, INPUT_FILTER -# is applied to all files. +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. -FILTER_PATTERNS = +FILTER_PATTERNS = # If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using -# INPUT_FILTER) will be used to filter the input files when producing source -# files to browse (i.e. when SOURCE_BROWSER is set to YES). +# INPUT_FILTER) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. FILTER_SOURCE_FILES = NO +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. + +FILTER_SOURCE_PATTERNS = + +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. + +USE_MDFILE_AS_MAINPAGE = + #--------------------------------------------------------------------------- -# configuration options related to source browsing +# Configuration options related to source browsing #--------------------------------------------------------------------------- -# If the SOURCE_BROWSER tag is set to YES then a list of source files will -# be generated. Documented entities will be cross-referenced with these sources. -# Note: To get rid of all source code in the generated output, make sure also -# VERBATIM_HEADERS is set to NO. +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. -SOURCE_BROWSER = NO +SOURCE_BROWSER = YES -# Setting the INLINE_SOURCES tag to YES will include the body -# of functions and classes directly in the documentation. +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. INLINE_SOURCES = NO -# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct -# doxygen to hide any special comment blocks from generated source code -# fragments. Normal C and C++ comments will always remain visible. +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. STRIP_CODE_COMMENTS = YES -# If the REFERENCED_BY_RELATION tag is set to YES -# then for each documented function all documented -# functions referencing it will be listed. +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# function all documented functions referencing it will be listed. +# The default value is: NO. REFERENCED_BY_RELATION = YES -# If the REFERENCES_RELATION tag is set to YES -# then for each documented function all documented entities -# called/used by that function will be listed. +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. REFERENCES_RELATION = YES -# If the REFERENCES_LINK_SOURCE tag is set to YES (the default) -# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from -# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will -# link to the source code. Otherwise they will link to the documentstion. +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. REFERENCES_LINK_SOURCE = YES -# If the USE_HTAGS tag is set to YES then the references to source code -# will point to the HTML generated by the htags(1) tool instead of doxygen -# built-in source browser. The htags tool is part of GNU's global source -# tagging system (see http://www.gnu.org/software/global/global.html). You -# will need version 4.8.6 or higher. +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see http://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the config file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. USE_HTAGS = NO -# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen -# will generate a verbatim copy of the header file for each class for -# which an include is specified. Set to NO to disable this. +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. VERBATIM_HEADERS = YES +# If the CLANG_ASSISTED_PARSING tag is set to YES then doxygen will use the +# clang parser (see: http://clang.llvm.org/) for more accurate parsing at the +# cost of reduced performance. This can be particularly helpful with template +# rich C++ code for which doxygen's built-in parser lacks the necessary type +# information. +# Note: The availability of this option depends on whether or not doxygen was +# generated with the -Duse-libclang=ON option for CMake. +# The default value is: NO. + +CLANG_ASSISTED_PARSING = NO + +# If clang assisted parsing is enabled you can provide the compiler with command +# line options that you would normally use when invoking the compiler. Note that +# the include paths will already be set by doxygen for the files and directories +# specified with INPUT and INCLUDE_PATH. +# This tag requires that the tag CLANG_ASSISTED_PARSING is set to YES. + +CLANG_OPTIONS = + #--------------------------------------------------------------------------- -# configuration options related to the alphabetical class index +# Configuration options related to the alphabetical class index #--------------------------------------------------------------------------- -# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index -# of all compounds will be generated. Enable this if the project -# contains a lot of classes, structs, unions or interfaces. +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. ALPHABETICAL_INDEX = NO -# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then -# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns -# in which this list will be split (can be a number in the range [1..20]) +# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in +# which the alphabetical index list will be split. +# Minimum value: 1, maximum value: 20, default value: 5. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. COLS_IN_ALPHA_INDEX = 5 -# In case all classes in a project start with a common prefix, all -# classes will be put under the same header in the alphabetical index. -# The IGNORE_PREFIX tag can be used to specify one or more prefixes that -# should be ignored while generating the index headers. +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. -IGNORE_PREFIX = +IGNORE_PREFIX = #--------------------------------------------------------------------------- -# configuration options related to the HTML output +# Configuration options related to the HTML output #--------------------------------------------------------------------------- -# If the GENERATE_HTML tag is set to YES (the default) Doxygen will -# generate HTML output. +# If the GENERATE_HTML tag is set to YES, doxygen will generate HTML output +# The default value is: YES. GENERATE_HTML = YES -# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. -# If a relative path is entered the value of OUTPUT_DIRECTORY will be -# put in front of it. If left blank `html' will be used as the default path. +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_OUTPUT = html -# The HTML_FILE_EXTENSION tag can be used to specify the file extension for -# each generated HTML page (for example: .htm,.php,.asp). If it is left blank -# doxygen will generate files with .html extension. +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_FILE_EXTENSION = .html -# The HTML_HEADER tag can be used to specify a personal HTML header for -# each generated HTML page. If it is left blank doxygen will generate a +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a # standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify additional user-defined +# cascading style sheets that are included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefore more robust against future updates. +# Doxygen will copy the style sheet files to the output directory. +# Note: The order of the extra style sheet files is of importance (e.g. the last +# style sheet in the list overrules the setting of the previous ones in the +# list). For an example see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the style sheet and background images according to +# this color. Hue is specified as an angle on a colorwheel, see +# http://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 217 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use grayscales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_SAT = 74 + +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 124 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to YES can help to show when doxygen was last run and thus if the +# documentation is up to date. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = NO -HTML_HEADER = - -# The HTML_FOOTER tag can be used to specify a personal HTML footer for -# each generated HTML page. If it is left blank doxygen will generate a -# standard footer. - -HTML_FOOTER = - -# The HTML_STYLESHEET tag can be used to specify a user-defined cascading -# style sheet that is used by each HTML page. It can be used to -# fine-tune the look of the HTML output. If the tag is left blank doxygen -# will generate a default style sheet. Note that doxygen will try to copy -# the style sheet file to the HTML output directory, so don't put your own -# stylesheet in the HTML output directory as well, or it will be erased! +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. -HTML_STYLESHEET = +HTML_DYNAMIC_SECTIONS = NO -# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes, -# files or namespaces will be aligned in HTML using tables. If set to -# NO a bullet list will be used. +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_INDEX_NUM_ENTRIES = 100 + +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: http://developer.apple.com/tools/xcode/), introduced with +# OSX 10.5 (Leopard). To create a documentation set, doxygen will generate a +# Makefile in the HTML output directory. Running make will produce the docset in +# that directory and running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html +# for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. -HTML_ALIGN_MEMBERS = YES +GENERATE_DOCSET = NO -# If the GENERATE_HTMLHELP tag is set to YES, additional index files -# will be generated that can be used as input for tools like the -# Microsoft HTML help workshop to generate a compiled HTML help file (.chm) -# of the generated HTML documentation. +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. -GENERATE_HTMLHELP = NO +DOCSET_FEEDNAME = "Doxygen generated docs" -# If the GENERATE_DOCSET tag is set to YES, additional index files -# will be generated that can be used as input for Apple's Xcode 3 -# integrated development environment, introduced with OSX 10.5 (Leopard). -# To create a documentation set, doxygen will generate a Makefile in the -# HTML output directory. Running make will produce the docset in that -# directory and running "make install" will install the docset in -# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find -# it at startup. +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. -GENERATE_DOCSET = NO +DOCSET_BUNDLE_ID = org.doxygen.Project -# When GENERATE_DOCSET tag is set to YES, this tag determines the name of the -# feed. A documentation feed provides an umbrella under which multiple -# documentation sets from a single provider (such as a company or product suite) -# can be grouped. +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style +# string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. -DOCSET_FEEDNAME = "Doxygen generated docs" +DOCSET_PUBLISHER_ID = org.doxygen.Publisher -# When GENERATE_DOCSET tag is set to YES, this tag specifies a string that -# should uniquely identify the documentation set bundle. This should be a -# reverse domain-name style string, e.g. com.mycompany.MyDocSet. Doxygen -# will append .docset to the name. +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. -DOCSET_BUNDLE_ID = org.doxygen.Project +DOCSET_PUBLISHER_NAME = Publisher -# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML -# documentation will contain sections that can be hidden and shown after the -# page has loaded. For this to work a browser that supports -# JavaScript and DHTML is required (for instance Mozilla 1.0+, Firefox -# Netscape 6.0+, Internet explorer 5.0+, Konqueror, or Safari). +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# (see: http://www.microsoft.com/en-us/download/details.aspx?id=21138) on +# Windows. +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. -HTML_DYNAMIC_SECTIONS = NO +GENERATE_HTMLHELP = NO -# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can -# be used to specify the file name of the resulting .chm file. You -# can add a path in front of the file if the result should not be +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be # written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -CHM_FILE = +CHM_FILE = -# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can -# be used to specify the location (absolute path including file name) of -# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run -# the HTML help compiler on the generated index.hhp. +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler (hhc.exe). If non-empty, +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -HHC_LOCATION = +HHC_LOCATION = -# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag -# controls if a separate .chi index file is generated (YES) or that -# it should be included in the master .chm file (NO). +# The GENERATE_CHI flag controls if a separate .chi index file is generated +# (YES) or that it should be included in the master .chm file (NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. GENERATE_CHI = NO -# If the GENERATE_HTMLHELP tag is set to YES, the CHM_INDEX_ENCODING -# is used to encode HtmlHelp index (hhk), content (hhc) and project file -# content. +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index (hhk), content (hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -CHM_INDEX_ENCODING = +CHM_INDEX_ENCODING = -# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag -# controls whether a binary table of contents is generated (YES) or a -# normal table of contents (NO) in the .chm file. +# The BINARY_TOC flag controls whether a binary table of contents is generated +# (YES) or a normal table of contents (NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. BINARY_TOC = NO -# The TOC_EXPAND flag can be set to YES to add extra items for group members -# to the contents of the HTML help documentation and to the tree view. +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. TOC_EXPAND = NO -# The DISABLE_INDEX tag can be used to turn on/off the condensed index at -# top of each HTML page. The value NO (the default) enables the index and -# the value YES disables it. +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#virtual- +# folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_VIRTUAL_FOLDER = doc + +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# http://qt-project.org/doc/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_SECT_FILTER_ATTRS = + +# The QHG_LOCATION tag can be used to specify the location of Qt's +# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the +# generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. DISABLE_INDEX = NO -# This tag can be used to set the number of enum values (range [1..20]) -# that doxygen will group on one line in the generated HTML documentation. +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom style sheets (see HTML_EXTRA_STYLESHEET) one can +# further fine-tune the look of the index. As an example, the default style +# sheet generated by doxygen has an example that shows how to put an image at +# the root of the tree instead of the PROJECT_NAME. Since the tree basically has +# the same information as the tab index, you could consider setting +# DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_TREEVIEW = YES + +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. ENUM_VALUES_PER_LINE = 4 -# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index -# structure should be generated to display hierarchical information. -# If the tag value is set to FRAME, a side panel will be generated -# containing a tree-like index structure (just like the one that -# is generated for HTML Help). For this to work a browser that supports -# JavaScript, DHTML, CSS and frames is required (for instance Mozilla 1.0+, -# Netscape 6.0+, Internet explorer 5.0+, or Konqueror). Windows users are -# probably better off using the HTML help feature. Other possible values -# for this tag are: HIERARCHIES, which will generate the Groups, Directories, -# and Class Hiererachy pages using a tree view instead of an ordered list; -# ALL, which combines the behavior of FRAME and HIERARCHIES; and NONE, which -# disables this behavior completely. For backwards compatibility with previous -# releases of Doxygen, the values YES and NO are equivalent to FRAME and NONE -# respectively. - -GENERATE_TREEVIEW = NONE - -# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be -# used to set the initial width (in pixels) of the frame in which the tree -# is shown. +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. TREEVIEW_WIDTH = 250 -# Use this tag to change the font size of Latex formulas included -# as images in the HTML documentation. The default is 10. Note that -# when you change the font size after a successful doxygen run you need -# to manually remove any form_*.png images from the HTML output directory -# to force them to be regenerated. +# If the EXT_LINKS_IN_WINDOW option is set to YES, doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +EXT_LINKS_IN_WINDOW = NO + +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. FORMULA_FONTSIZE = 10 +# Use the FORMULA_TRANPARENT tag to determine whether or not the images +# generated for formulas are transparent PNGs. Transparent PNGs are not +# supported properly for IE 6.0, but are supported on all modern browsers. +# +# Note that when changing this option you need to delete any form_*.png files in +# the HTML output directory before the changes have effect. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_TRANSPARENT = YES + +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# http://www.mathjax.org) which uses client side Javascript for the rendering +# instead of using pre-rendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +USE_MATHJAX = NO + +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. See the MathJax site (see: +# http://docs.mathjax.org/en/latest/output.html) for more details. +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility), NativeMML (i.e. MathML) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from http://www.mathjax.org before deployment. +# The default value is: http://cdn.mathjax.org/mathjax/latest. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /