diff options
| author |   Jonathan-Christofer Demay <jcdemay@gmail.com> | 2009-11-23 23:54:13 +0000 |
|---|---|---|
| committer | Jonathan-Christofer Demay <jcdemay@gmail.com> | 2009-11-23 23:54:13 +0000 |
| commit | 0292efad6383784da031dbb1b2dfe6c1b99e6e38 (patch) | |
| tree | fb84000996acb16fc1f0613bc0b25553b758b03f | |
| parent | sci-chemistry/ccpn -- Bad mistake in setting compile options --> leads to ope... (diff) | |
| download | sci-0292efad6383784da031dbb1b2dfe6c1b99e6e38.tar.gz sci-0292efad6383784da031dbb1b2dfe6c1b99e6e38.tar.bz2 sci-0292efad6383784da031dbb1b2dfe6c1b99e6e38.zip | |
sci-mathematics/frama-c-20090901: init_locals_defined.patch
| -rw-r--r-- | sci-mathematics/frama-c/Manifest | 3 | ||||
| -rw-r--r-- | sci-mathematics/frama-c/files/frama-c-20090901-init_locals_defined.patch | 62 | ||||
| -rw-r--r-- | sci-mathematics/frama-c/frama-c-20090901.ebuild | 1 |
3 files changed, 65 insertions, 1 deletions
diff --git a/sci-mathematics/frama-c/Manifest b/sci-mathematics/frama-c/Manifest index c39d1fffb..fdbb3dd41 100644 --- a/sci-mathematics/frama-c/Manifest +++ b/sci-mathematics/frama-c/Manifest @@ -1,5 +1,6 @@ +AUX frama-c-20090901-init_locals_defined.patch 2565 RMD160 3543c00bfef3b338f599297ec34121e77ac8b31e SHA1 168731e77eabdfe491496a9ad53c3a2d31a90282 SHA256 b66a8147691e7e8ad753bdb38b05635bc36514121440da73a3f5e921a70c9cda AUX frama-c-20090901-ocamlgraph_link.patch 721 RMD160 0b78639b9f31c62575a0552c93b48dd82faeb513 SHA1 ac84c82de12c8436973a97c2e62eceac8c0fd12d SHA256 5003ddacc4b90dfb6e61af643a0d22bf2135f1d7bdb10fe1f6e20d783da5207a AUX frama-c-20090901-varinfo_export.patch 672 RMD160 987c2ca3b627eaf500e5db8ad91ca8a81e3a1bd4 SHA1 d2cdbd2107058476b460d9986f7bb95ca5d6138e SHA256 03d8aee3083f9b35d535882124305d99964b193931eca877d45202abcf6d9186 AUX frama-c-20090901-why_link.patch 2172 RMD160 bc971e4d99a8a8b7570fd1da8e5f751b70b4a73f SHA1 6e8d3c337715af9d94f996aa2ca5a63dbae20ae9 SHA256 0f4020d2562cf32f85e1ee605464c2e48cffa0448245999fd063b70095640357 DIST frama-c-Beryllium-20090901.tar.gz 18162700 RMD160 b29038e948b898196947cae636eef9adbea99ed6 SHA1 17b1516e9807a9a34ab20a3413efc372549e6fed SHA256 ac420d72b9d0062dd1213a6e595a01c32d0cd5a465c8736c65a42cc717742cc9 -EBUILD frama-c-20090901.ebuild 1598 RMD160 ef53cb46cc6e2ae56e8131dee318c178d9b7b291 SHA1 5c9a95f996a433270f59a53b902aa1e9c4fb41bb SHA256 87758bc043a3403d8a759062eb89f382a2605e86000f9011c856541640e95cea +EBUILD frama-c-20090901.ebuild 1651 RMD160 15313d1aaeaa9aea42c0bef8edfb8b37fcda7379 SHA1 467d26d13f5144c2bd053d2eff336aa494b98510 SHA256 bf97b474a82afa473b26680baeb31f7da48f204a5742cd2480d5590375708112 diff --git a/sci-mathematics/frama-c/files/frama-c-20090901-init_locals_defined.patch b/sci-mathematics/frama-c/files/frama-c-20090901-init_locals_defined.patch new file mode 100644 index 000000000..a597c093b --- /dev/null +++ b/sci-mathematics/frama-c/files/frama-c-20090901-init_locals_defined.patch @@ -0,0 +1,62 @@ +diff -Naurp frama-c-Beryllium-20090901-orig/src/value/eval.ml frama-c-Beryllium-20090901-ptch/src/value/eval.ml +--- frama-c-Beryllium-20090901-orig/src/value/eval.ml 2009-08-31 15:38:54.000000000 +0000 ++++ frama-c-Beryllium-20090901-ptch/src/value/eval.ml 2009-11-23 23:44:25.000000000 +0000 +@@ -4315,13 +4315,20 @@ let compute_with_initial_state kf initia + | Definition (f,_) -> + let initial_state = check_precondition kf initial_state in + let initial_state = +- List.fold_left +- (fun acc local -> +- Relations_type.Model.add_binding_unspecified +- acc +- (Locations.loc_of_varinfo local)) +- initial_state +- f.slocals ++ if Parameters.Dynamic.Bool.get "-init-locals-defined" ++ then ++ List.fold_right ++ initialize_var_using_type ++ f.slocals ++ initial_state ++ else ++ List.fold_left ++ (fun acc local -> ++ Relations_type.Model.add_binding_unspecified ++ acc ++ (Locations.loc_of_varinfo local)) ++ initial_state ++ f.slocals + in + compute_using_cfg kf (ref (State_set.singleton initial_state)) + +diff -Naurp frama-c-Beryllium-20090901-orig/src/value/value_parameters.ml frama-c-Beryllium-20090901-ptch/src/value/value_parameters.ml +--- frama-c-Beryllium-20090901-orig/src/value/value_parameters.ml 2009-08-31 15:38:54.000000000 +0000 ++++ frama-c-Beryllium-20090901-ptch/src/value/value_parameters.ml 2009-11-23 23:43:18.000000000 +0000 +@@ -136,6 +136,15 @@ module PropagateTop = + let () = add_dependency PropagateTop.self + + let () = Plugin.set_group precision_tuning ++module InitLocalsDefined = ++ False ++ (struct ++ let option_name = "-init-locals-defined" ++ let descr = "init local variables defined like initialized extern globals" ++ end) ++let () = add_dependency InitLocalsDefined.self ++ ++let () = Plugin.set_group precision_tuning + module WideningLevel = + Int + (struct +diff -Naurp frama-c-Beryllium-20090901-orig/src/value/value_parameters.mli frama-c-Beryllium-20090901-ptch/src/value/value_parameters.mli +--- frama-c-Beryllium-20090901-orig/src/value/value_parameters.mli 2009-08-31 15:38:54.000000000 +0000 ++++ frama-c-Beryllium-20090901-ptch/src/value/value_parameters.mli 2009-11-23 23:43:04.000000000 +0000 +@@ -29,6 +29,8 @@ module WarnUnspecifiedOrder: Plugin.BOOL + + module PropagateTop: Plugin.BOOL + ++module InitLocalsDefined: Plugin.BOOL ++ + module AutomaticContextMaxDepth: Plugin.INT + module AutomaticContextMaxWidth: Plugin.INT + diff --git a/sci-mathematics/frama-c/frama-c-20090901.ebuild b/sci-mathematics/frama-c/frama-c-20090901.ebuild index 803d993e3..47da6ce37 100644 --- a/sci-mathematics/frama-c/frama-c-20090901.ebuild +++ b/sci-mathematics/frama-c/frama-c-20090901.ebuild @@ -36,6 +36,7 @@ src_prepare(){ epatch "${FILESDIR}/${P}-varinfo_export.patch" epatch "${FILESDIR}/${P}-why_link.patch" epatch "${FILESDIR}/${P}-ocamlgraph_link.patch" + epatch "${FILESDIR}/${P}-init_locals_defined.patch" eautoreconf } |