From be3c0f2b6e99da268d548f143bb26ac6ba32384a Mon Sep 17 00:00:00 2001 From: ImgBotApp Date: Tue, 2 Jun 2026 20:19:57 +0000 Subject: [PATCH] [ImgBot] Optimize images *Total -- 2,017.23kb -> 1,857.15kb (7.94%) /clang/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg -- 4.31kb -> 2.90kb (32.68%) /clang/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg -- 4.32kb -> 2.92kb (32.57%) /llvm/docs/loop-nonmaximal.svg -- 129.42kb -> 91.89kb (29%) /clang/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg -- 13.63kb -> 9.79kb (28.19%) /llvm/docs/loop-guard.svg -- 108.14kb -> 77.90kb (27.96%) /llvm/docs/loop-nested.svg -- 87.77kb -> 64.81kb (26.16%) /clang/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg -- 17.79kb -> 13.16kb (26%) /clang/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg -- 17.83kb -> 13.21kb (25.96%) /clang/docs/DataFlowAnalysisIntroImages/CFGExample.svg -- 24.92kb -> 18.82kb (24.46%) /llvm/docs/loop-single.svg -- 35.31kb -> 27.50kb (22.12%) /clang/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg -- 13.23kb -> 10.83kb (18.08%) /website/source/_static/logo-dark.svg -- 0.74kb -> 0.62kb (16.27%) /website/source/_static/logo.svg -- 0.74kb -> 0.63kb (15.88%) /lld/docs/partitions.svg -- 5.81kb -> 4.94kb (14.94%) /website/source/_static/favicon.svg -- 0.52kb -> 0.46kb (12.31%) /website/source/_static/logo-mark.svg -- 0.53kb -> 0.46kb (12.2%) /llvm/docs/loop-terminology.svg -- 116.10kb -> 104.46kb (10.03%) /website/source/_static/diagrams/vc-validity.svg -- 1.52kb -> 1.39kb (8.73%) /mlir/docs/includes/img/index-map.svg -- 65.20kb -> 60.08kb (7.86%) /website/source/_static/diagrams/cppverify-pipeline.svg -- 1.94kb -> 1.80kb (7.36%) /website/source/_static/diagrams/book-map.svg -- 1.68kb -> 1.57kb (6.45%) /website/source/_static/diagrams/loop-invariant-lifecycle.svg -- 2.12kb -> 2.00kb (5.77%) /website/source/_static/diagrams/modular-verification.svg -- 2.24kb -> 2.11kb (5.63%) /website/source/_static/diagrams/cppverify-workflow.svg -- 2.26kb -> 2.14kb (5.22%) /website/source/_static/diagrams/testing-vs-samples.svg -- 1.58kb -> 1.50kb (5%) /llvm/docs/loop-merge.svg -- 88.08kb -> 83.69kb (4.99%) /llvm/docs/loop-separate.svg -- 90.69kb -> 86.23kb (4.92%) /website/source/_static/diagrams/hoare-triple.svg -- 1.47kb -> 1.40kb (4.91%) /mlir/docs/includes/img/view-operation.svg -- 155.05kb -> 147.60kb (4.8%) /website/source/_static/logo-todo.svg -- 0.36kb -> 0.36kb (1.88%) /mlir/docs/includes/img/mlir-lsp-server-server_diagram.svg -- 33.99kb -> 33.79kb (0.61%) /mlir/docs/includes/img/Use-list.svg -- 69.32kb -> 68.97kb (0.51%) /mlir/docs/includes/img/DefUseChains.svg -- 155.64kb -> 154.94kb (0.45%) /libc/docs/gpu/rpc-diagram.svg -- 62.11kb -> 61.86kb (0.4%) /mlir/docs/includes/img/bufferization_tensor_insert_dst.svg -- 77.48kb -> 77.36kb (0.16%) /mlir/docs/includes/img/bufferization_passes.svg -- 203.40kb -> 203.21kb (0.09%) /mlir/docs/includes/img/bufferization_dealloc_op.svg -- 419.96kb -> 419.84kb (0.03%) Signed-off-by: ImgBotApp --- .../CFGExample.svg | 521 +--- .../CFGJoinRule.svg | 223 +- .../DefinitiveInitializationLattice.svg | 115 +- .../IntegerSetsFiniteLattice.svg | 404 +--- .../IntegerSetsInfiniteLattice.svg | 404 +--- .../OutputParameterIdentificationLattice.svg | 341 +-- .../UniquePtrLattice.svg | 115 +- libc/docs/gpu/rpc-diagram.svg | 2 +- lld/docs/partitions.svg | 111 +- llvm/docs/loop-guard.svg | 1080 +-------- llvm/docs/loop-merge.svg | 661 +----- llvm/docs/loop-nested.svg | 875 +------ llvm/docs/loop-nonmaximal.svg | 1281 +--------- llvm/docs/loop-separate.svg | 691 +----- llvm/docs/loop-single.svg | 339 +-- llvm/docs/loop-terminology.svg | 2112 +---------------- mlir/docs/includes/img/DefUseChains.svg | 2 +- mlir/docs/includes/img/Use-list.svg | 2 +- .../includes/img/bufferization_dealloc_op.svg | 2 +- .../includes/img/bufferization_passes.svg | 2 +- .../img/bufferization_tensor_insert_dst.svg | 2 +- mlir/docs/includes/img/index-map.svg | 381 +-- .../img/mlir-lsp-server-server_diagram.svg | 2 +- mlir/docs/includes/img/view-operation.svg | 581 +---- website/source/_static/diagrams/book-map.svg | 28 +- .../_static/diagrams/cppverify-pipeline.svg | 32 +- .../_static/diagrams/cppverify-workflow.svg | 33 +- .../source/_static/diagrams/hoare-triple.svg | 21 +- .../diagrams/loop-invariant-lifecycle.svg | 32 +- .../_static/diagrams/modular-verification.svg | 35 +- .../_static/diagrams/testing-vs-samples.svg | 23 +- .../source/_static/diagrams/vc-validity.svg | 23 +- website/source/_static/favicon.svg | 10 +- website/source/_static/logo-dark.svg | 18 +- website/source/_static/logo-mark.svg | 10 +- website/source/_static/logo-todo.svg | 5 +- website/source/_static/logo.svg | 18 +- 37 files changed, 37 insertions(+), 10500 deletions(-) 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, invariants⇒Goal (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