diff --git a/clang/docs/DataFlowAnalysisIntroImages/CFGExample.svg b/clang/docs/DataFlowAnalysisIntroImages/CFGExample.svg index 8e81576018..3c2e4d0d2b 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/CFGExample.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/CFGExample.svg @@ -1,520 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Entry - - // Pre: x is ⊥int x;if (n > 0)// Post: x is ⊥ - - // Pre: x is ⊥x = n;// Post: x is ⊤ - - // Pre: x is ⊥if (n == 42)// Post: x is ⊥ - - // Pre: x is ⊥x = 5;// Post: x is {5} - - // Pre: x is ⊥x = 44;// Post: x is {44} - - // Pre: x is {5; 44}print(x);// Post: x is {5; 44} - - // Pre: x is ⊤print(x);// Post: x is ⊤ - - - - - - - - - - - Exit - - True - True - False - False - - +Entry// Pre: x is ⊥int x;if (n > 0)// Post: x is ⊥// Pre: x is ⊥x = n;// Post: x is ⊤// Pre: x is ⊥if (n == 42)// Post: x is ⊥// Pre: x is ⊥x = 5;// Post: x is {5}// Pre: x is ⊥x = 44;// Post: x is {44}// Pre: x is {5; 44}print(x);// Post: x is {5; 44}// Pre: x is ⊤print(x);// Post: x is ⊤ExitTrueTrueFalseFalse \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg b/clang/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg index 95daffa8d9..5153013ac2 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg @@ -1,222 +1 @@ - - - - - - - - - - - - (Given) - (Conclusion) - in1 - in2 - inn - join(in1, in2, …, inn) - out = transfer(basic_block, join(in1, in2, …, inn)) - - Basic block - - - - - - - +(Given)(Conclusion)in1in2innjoin(in1, in2, …, inn)out = transfer(basic_block, join(in1, in2, …, inn))Basic block \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg b/clang/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg index 861a3f9c74..6a13749cac 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg @@ -1,114 +1 @@ - - - - - - - - - - - - Maybe uninitialized - Initialized - Uninitialized - - - - - - - +Maybe uninitializedInitializedUninitialized \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg b/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg index aab7d3e986..737349fe04 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg @@ -1,403 +1 @@ - - - - - ⊥ = {} - - - {−9} - {−5} - - {−3} - {−2} - {−1} - {0} - {1} - {2} - {3} - - - - - - - - - - - - - {−9, −5} - {−3, −1} - - {1, 2} - - - - - - - - - {1, 2, 3} - - - - ⊤ = ℤ - - - - - - - +⊥ = {}{−9}{−5}{−3}{−2}{−1}{0}{1}{2}{3}{−9, −5}{−3, −1}{1, 2}{1, 2, 3}⊤ = ℤ \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg b/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg index 380aa2a0b4..a8ce50eda0 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg @@ -1,403 +1 @@ - - - - - ⊥ = {} - - - {−9} - {−5} - - {−3} - {−2} - {−1} - {0} - {1} - {2} - {3} - - - - - - - - - - - - - {−9, −5} - {−3, −1} - - {1, 2} - - - - - - - - - {1, 2, 3} - - - - (goes up infinitely) - - - - - - - +⊥ = {}{−9}{−5}{−3}{−2}{−1}{0}{1}{2}{3}{−9, −5}{−3, −1}{1, 2}{1, 2, 3}(goes up infinitely) \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg b/clang/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg index 5658587c2e..511ab3c037 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg @@ -1,340 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Overwritten: {p->x, p->y, p->z} - Overwritten: {p->x, p->z} - Overwritten: {p->x, p->z} - Overwritten: {p->q} - Overwritten: {} - - - - - Normal states - - - Failure states - {Unsafe read at line 3} - {Pointer escape at line 5} - {Unsafe read at line 7} - {Unsafe read at line 3, Pointer escape at line 5} - - - {Unsafe read at line 3, Pointer escape at line 5, Unsafe read at line 7} - - - - - +Overwritten: {p->x, p->y, p->z}Overwritten: {p->x, p->z}Overwritten: {p->x, p->z}Overwritten: {p->q}Overwritten: {}Normal statesFailure states{Unsafe read at line 3}{Pointer escape at line 5}{Unsafe read at line 7}{Unsafe read at line 3, Pointer escape at line 5}{Unsafe read at line 3, Pointer escape at line 5, Unsafe read at line 7} \ No newline at end of file diff --git a/clang/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg b/clang/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg index f7a618ab0c..dfcb9f753b 100644 --- a/clang/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg +++ b/clang/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg @@ -1,114 +1 @@ - - - - - - - - - - - - Conflicting - Defined - Compatible - - - - - - - +ConflictingDefinedCompatible \ No newline at end of file diff --git a/libc/docs/gpu/rpc-diagram.svg b/libc/docs/gpu/rpc-diagram.svg index eb9b807e52..7ca55dfb12 100644 --- a/libc/docs/gpu/rpc-diagram.svg +++ b/libc/docs/gpu/rpc-diagram.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/lld/docs/partitions.svg b/lld/docs/partitions.svg index 39cd969334..e35c1eb6c1 100644 --- a/lld/docs/partitions.svg +++ b/lld/docs/partitions.svg @@ -1,110 +1 @@ - - - - - - -G - - -part_main -Main partition - - -main - -main - - -part_main->main - - - - -part1 -Loadable partition 1 - - -f1 - -f1 - - -part1->f1 - - - - -part2 -Loadable partition 2 - - -f2 - -f2 - - -part2->f2 - - - - -f3 - -f3 - - -main->f3 - - - - -f1->f3 - - - - -f4 - -f4 - - -f1->f4 - - - - -f5 - -f5 - - -f1->f5 - - - - -f2->f3 - - - - -f2->f5 - - - - -f6 - -f6 - - -f2->f6 - - - - - +Gpart_mainMain partitionmainmainpart_main->mainpart1Loadable partition 1f1f1part1->f1part2Loadable partition 2f2f2part2->f2f3f3main->f3f1->f3f4f4f1->f4f5f5f1->f5f2->f3f2->f5f6f6f2->f6 \ No newline at end of file diff --git a/llvm/docs/loop-guard.svg b/llvm/docs/loop-guard.svg index dbb930f057..4e93b7c78d 100644 --- a/llvm/docs/loop-guard.svg +++ b/llvm/docs/loop-guard.svg @@ -1,1079 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-merge.svg b/llvm/docs/loop-merge.svg index ea5e574b2d..f3dc9dc042 100644 --- a/llvm/docs/loop-merge.svg +++ b/llvm/docs/loop-merge.svg @@ -1,660 +1 @@ - - - - - - image/svg+xml - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-nested.svg b/llvm/docs/loop-nested.svg index 372a3b43ec..b6336375b1 100644 --- a/llvm/docs/loop-nested.svg +++ b/llvm/docs/loop-nested.svg @@ -1,874 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-nonmaximal.svg b/llvm/docs/loop-nonmaximal.svg index cb6e4d64b5..5f91c3d985 100644 --- a/llvm/docs/loop-nonmaximal.svg +++ b/llvm/docs/loop-nonmaximal.svg @@ -1,1280 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-separate.svg b/llvm/docs/loop-separate.svg index fafd3eb42a..568b0e576e 100644 --- a/llvm/docs/loop-separate.svg +++ b/llvm/docs/loop-separate.svg @@ -1,690 +1 @@ - - - - - - image/svg+xml - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-single.svg b/llvm/docs/loop-single.svg index 6f9720a0dc..4a7ed2a35d 100644 --- a/llvm/docs/loop-single.svg +++ b/llvm/docs/loop-single.svg @@ -1,338 +1 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/llvm/docs/loop-terminology.svg b/llvm/docs/loop-terminology.svg index 6bed1733bb..ffc8b9fee7 100644 --- a/llvm/docs/loop-terminology.svg +++ b/llvm/docs/loop-terminology.svg @@ -1,2111 +1 @@ - - - - - - image/svg+xml - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/mlir/docs/includes/img/DefUseChains.svg b/mlir/docs/includes/img/DefUseChains.svg index 2d5b752467..d6f3ed9b46 100644 --- a/mlir/docs/includes/img/DefUseChains.svg +++ b/mlir/docs/includes/img/DefUseChains.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/Use-list.svg b/mlir/docs/includes/img/Use-list.svg index 4840619f06..1a6b3d95e9 100644 --- a/mlir/docs/includes/img/Use-list.svg +++ b/mlir/docs/includes/img/Use-list.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/bufferization_dealloc_op.svg b/mlir/docs/includes/img/bufferization_dealloc_op.svg index 3b72ae72c4..2f4b713394 100644 --- a/mlir/docs/includes/img/bufferization_dealloc_op.svg +++ b/mlir/docs/includes/img/bufferization_dealloc_op.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/bufferization_passes.svg b/mlir/docs/includes/img/bufferization_passes.svg index 8357265692..c33a6855bf 100644 --- a/mlir/docs/includes/img/bufferization_passes.svg +++ b/mlir/docs/includes/img/bufferization_passes.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/bufferization_tensor_insert_dst.svg b/mlir/docs/includes/img/bufferization_tensor_insert_dst.svg index 228b19e922..1cbe556d22 100644 --- a/mlir/docs/includes/img/bufferization_tensor_insert_dst.svg +++ b/mlir/docs/includes/img/bufferization_tensor_insert_dst.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/index-map.svg b/mlir/docs/includes/img/index-map.svg index 6004c2da36..cd055718fc 100644 --- a/mlir/docs/includes/img/index-map.svg +++ b/mlir/docs/includes/img/index-map.svg @@ -1,380 +1 @@ - - - - - - image/svg+xml - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/mlir/docs/includes/img/mlir-lsp-server-server_diagram.svg b/mlir/docs/includes/img/mlir-lsp-server-server_diagram.svg index 4577058586..34bb7ff96f 100644 --- a/mlir/docs/includes/img/mlir-lsp-server-server_diagram.svg +++ b/mlir/docs/includes/img/mlir-lsp-server-server_diagram.svg @@ -1 +1 @@ - \ No newline at end of file + \ No newline at end of file diff --git a/mlir/docs/includes/img/view-operation.svg b/mlir/docs/includes/img/view-operation.svg index f4d622ee26..5eb1a1bc78 100644 --- a/mlir/docs/includes/img/view-operation.svg +++ b/mlir/docs/includes/img/view-operation.svg @@ -1,580 +1 @@ - - - - - - image/svg+xml - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + \ No newline at end of file diff --git a/website/source/_static/diagrams/book-map.svg b/website/source/_static/diagrams/book-map.svg index 2dfe502c6a..a793140558 100644 --- a/website/source/_static/diagrams/book-map.svg +++ b/website/source/_static/diagrams/book-map.svg @@ -1,27 +1 @@ - - CppVerify book: Part I foundations then Part II practice - - - - - - - - Part I — Foundations - Logic, Hoare triples, invariants - Memory, frames, SMT - No CppVerify syntax required - Chapters 1–8 - - - Part II — CppVerify - Flags, contracts in C++ - Toolchain, counterexamples - Builds on Part I - Chapters 9–16 - \ No newline at end of file +CppVerify book: Part I foundations then Part II practicePart I — FoundationsLogic, Hoare triples, invariantsMemory, frames, SMTNo CppVerify syntax requiredChapters 1–8Part II — CppVerifyFlags, contracts in C++Toolchain, counterexamplesBuilds on Part IChapters 9–16 \ No newline at end of file diff --git a/website/source/_static/diagrams/cppverify-pipeline.svg b/website/source/_static/diagrams/cppverify-pipeline.svg index 4dd5abc712..3f59a50958 100644 --- a/website/source/_static/diagrams/cppverify-pipeline.svg +++ b/website/source/_static/diagrams/cppverify-pipeline.svg @@ -1,31 +1 @@ - - CppVerify pipeline from AST to Z3 result - - - - - - - - - AST - - VCR - L1 - - Passive - L2 - - WP - - Z3 - - Result - - - --dump-ir selects layers 1–4 - \ No newline at end of file +CppVerify pipeline from AST to Z3 resultASTVCRL1PassiveL2WPZ3Result--dump-ir selects layers 1–4 \ No newline at end of file diff --git a/website/source/_static/diagrams/cppverify-workflow.svg b/website/source/_static/diagrams/cppverify-workflow.svg index 89411bc480..f7ae9bbb3b 100644 --- a/website/source/_static/diagrams/cppverify-workflow.svg +++ b/website/source/_static/diagrams/cppverify-workflow.svg @@ -1,32 +1 @@ - - Clang AST feeds parallel verify and compile paths - - - - - - - - .cpp + - contracts - - Clang - parse + Sema - -fverify-contracts - - Verify path - VCR → Passive → WP - → Z3 → diagnostics - cpp-verify / -fverify - - Compile path - CodeGen strips ghost - and contract nodes - runs parallel with verify - - Same AST; verify reads contracts, codegen emits LLVM without ghost code - \ No newline at end of file +Clang AST feeds parallel verify and compile paths.cpp +contractsClangparse + Sema-fverify-contractsVerify pathVCR → Passive → WP→ Z3 → diagnosticscpp-verify / -fverifyCompile pathCodeGen strips ghostand contract nodesruns parallel with verifySame AST; verify reads contracts, codegen emits LLVM without ghost code \ No newline at end of file diff --git a/website/source/_static/diagrams/hoare-triple.svg b/website/source/_static/diagrams/hoare-triple.svg index 1e2cd6c62b..799226b5d0 100644 --- a/website/source/_static/diagrams/hoare-triple.svg +++ b/website/source/_static/diagrams/hoare-triple.svg @@ -1,20 +1 @@ - - Hoare triple: precondition, statement, postcondition - - If P holds before S runs, then Q holds after S (when S terminates) - - { P } - - - Statement S - your code - - - { Q } - Hoare triple: { P } S { Q } - \ No newline at end of file +Hoare triple: precondition, statement, postconditionIf P holds before S runs, then Q holds after S (when S terminates){ P }Statement Syour code{ Q }Hoare triple: { P } S { Q } \ No newline at end of file diff --git a/website/source/_static/diagrams/loop-invariant-lifecycle.svg b/website/source/_static/diagrams/loop-invariant-lifecycle.svg index 92f83fbe34..20952dd817 100644 --- a/website/source/_static/diagrams/loop-invariant-lifecycle.svg +++ b/website/source/_static/diagrams/loop-invariant-lifecycle.svg @@ -1,31 +1 @@ - - Loop invariant: establishment, preservation, exit - - - - - - - - Entry - Invariant I - must hold - establishment - - preservation - One iteration - Assume I and cond - Run body; prove I again - - Exit - I and not cond - useful fact - exit condition - - - \ No newline at end of file +Loop invariant: establishment, preservation, exitEntryInvariant Imust holdestablishmentpreservationOne iterationAssume I and condRun body; prove I againExitI and not conduseful factexit condition \ No newline at end of file diff --git a/website/source/_static/diagrams/modular-verification.svg b/website/source/_static/diagrams/modular-verification.svg index 062d786494..f444ef180b 100644 --- a/website/source/_static/diagrams/modular-verification.svg +++ b/website/source/_static/diagrams/modular-verification.svg @@ -1,34 +1 @@ - - Modular verification: caller proves callee pre and assumes post - - - - - - - - Caller (main) - 1. Prove callee.pre at call site - 2. Call f() - 3. Assume callee.post after return - - VC: pre_main ⇒ post_main - - Callee (f) - Body not needed at call site - - pre: P - - body (hidden) - proved separately - - post: Q - - VC: P ⇒ Q - - contract - \ No newline at end of file +Modular verification: caller proves callee pre and assumes postCaller (main)1. Prove callee.pre at call site2. Call f()3. Assume callee.post after returnVC: pre_main ⇒ post_mainCallee (f)Body not needed at call sitepre: Pbody (hidden)proved separatelypost: QVC: P ⇒ Qcontract \ No newline at end of file diff --git a/website/source/_static/diagrams/testing-vs-samples.svg b/website/source/_static/diagrams/testing-vs-samples.svg index 7140123155..2e31c58b75 100644 --- a/website/source/_static/diagrams/testing-vs-samples.svg +++ b/website/source/_static/diagrams/testing-vs-samples.svg @@ -1,22 +1 @@ - - Testing samples finitely many inputs; verification covers the modeled domain - - - Testing - - - - - - Finitely many sample inputs - Verification - (within SMT theory) - - All inputs satisfying - the precondition - Proof obligation, not sampling - \ No newline at end of file +Testing samples finitely many inputs; verification covers the modeled domainTestingFinitely many sample inputsVerification(within SMT theory)All inputs satisfyingthe preconditionProof obligation, not sampling \ No newline at end of file diff --git a/website/source/_static/diagrams/vc-validity.svg b/website/source/_static/diagrams/vc-validity.svg index 14235d124a..501aa3286b 100644 --- a/website/source/_static/diagrams/vc-validity.svg +++ b/website/source/_static/diagrams/vc-validity.svg @@ -1,22 +1 @@ - - Verification condition: prove Hypothesis implies Goal via UNSAT - - Prove: Hypothesis ⇒ Goal - - Hypothesis - pre, path facts, invariants - - - Goal (post) - Q - - CppVerify: UNSAT( Hypothesis ∧ ¬Goal ) - No satisfying model ⇒ implication holds in the theory - \ No newline at end of file +Verification condition: prove Hypothesis implies Goal via UNSATProve: Hypothesis ⇒ GoalHypothesispre, path facts, invariantsGoal (post)QCppVerify: UNSAT( Hypothesis ∧ ¬Goal )No satisfying model ⇒ implication holds in the theory \ No newline at end of file diff --git a/website/source/_static/favicon.svg b/website/source/_static/favicon.svg index 3ad526bdb8..7ef871cc3f 100644 --- a/website/source/_static/favicon.svg +++ b/website/source/_static/favicon.svg @@ -1,9 +1 @@ - - - - - - - - - \ No newline at end of file + \ No newline at end of file diff --git a/website/source/_static/logo-dark.svg b/website/source/_static/logo-dark.svg index 2683670a5e..fcf09d5888 100644 --- a/website/source/_static/logo-dark.svg +++ b/website/source/_static/logo-dark.svg @@ -1,17 +1 @@ - - - - - - - - - - - - - - - CppVerify - - \ No newline at end of file +CppVerify \ No newline at end of file diff --git a/website/source/_static/logo-mark.svg b/website/source/_static/logo-mark.svg index 4061ee390e..509d76cf38 100644 --- a/website/source/_static/logo-mark.svg +++ b/website/source/_static/logo-mark.svg @@ -1,9 +1 @@ - - - - - - - - - \ No newline at end of file + \ No newline at end of file diff --git a/website/source/_static/logo-todo.svg b/website/source/_static/logo-todo.svg index a6754de7b1..0bb987b987 100644 --- a/website/source/_static/logo-todo.svg +++ b/website/source/_static/logo-todo.svg @@ -1,4 +1 @@ - - - TODO: logo - \ No newline at end of file +TODO: logo \ No newline at end of file diff --git a/website/source/_static/logo.svg b/website/source/_static/logo.svg index e83cbc4c24..0ce1d92ce3 100644 --- a/website/source/_static/logo.svg +++ b/website/source/_static/logo.svg @@ -1,17 +1 @@ - - - - - - - - - - - - - - - CppVerify - - \ No newline at end of file +CppVerify \ No newline at end of file