Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc
  • 2699-wp-region-plugin-division-by-0-with-empty-region-node
  • stable/copper
  • stable/nickel
  • stable/cobalt
  • stable/iron
  • stable/manganese
  • stable/chromium
  • stable/vanadium
  • stable/titanium-backport
  • stable/titanium
  • stable/scandium
  • 30.0 protected
  • 30.0-beta protected
  • MIEL-2024-10 protected
  • 29.0 protected
  • 29.0-beta protected
  • 28.1 protected
  • 28.0 protected
  • MIEL-2023-10 protected
  • 28.0-beta protected
  • 27.1 protected
  • 27.0 protected
  • 27.0-beta protected
  • 26.1 protected
  • 26.0 protected
  • 26.0-beta protected
  • 25.0-r1 protected
  • pre-dune protected
  • 25.0 protected
  • 25.0-beta protected
  • 2022-03-23 protected
33 results
Search by author
  • Any Author
  • Allan Blanchard Allan Blanchard blanchard
  • Amine Nasri Amine Nasri anasri
  • Andre Maroneze Andre Maroneze maroneze
  • Armand Puccetti Armand Puccetti puccetti
  • Augustin Lemesle Augustin Lemesle alemesle
  • Augustin PERRIN Augustin PERRIN aperrin
  • Aymeric Varasse Aymeric Varasse varasse
  • Basile Desloges Basile Desloges bdesloges
  • Benjamin Jorge Benjamin Jorge jorge
  • Bernard Botella Bernard Botella botella
  • Boris Yakobowski Boris Yakobowski byako
  • Cécile Ruet-Cros Cécile Ruet-Cros cruetcros
  • Charles Babu M Charles Babu M charlesm
  • Christophe Junke Christophe Junke cjunke
  • David Bühler David Bühler buhler
  • David Feliot David Feliot dfeliot
  • Dorian Lesbre Dorian Lesbre dlesbre
  • Fabio ALVES Fabio ALVES falves
  • Florent Kirchner Florent Kirchner kirchner
  • Frama-CI Frama-CI frama-ci
20 authors
  1. Feb 04, 2019
  3. Feb 01, 2019
    • Andre Maroneze's avatar
      Merge branch 'fix/libc/no-addr-array' into 'master' · 1b1693fc
      Andre Maroneze authored 
      [libc] fixes bug in time.h (taking address of array instead of first elt)

See merge request frama-c/frama-c!2138
      1b1693fc
    • Virgile Prevosto's avatar
      Merge branch 'feature/andre/libc-bzero-init' into 'master' · ae3347dc
      Virgile Prevosto authored 
      [libc] more precise spec for bzero

See merge request frama-c/frama-c!2106
      ae3347dc
    • Virgile Prevosto's avatar
      [libc] fixes bug in time.h (taking address of array instead of first elt) · 10d01115
      Virgile Prevosto authored
      10d01115
    • Andre Maroneze's avatar
      [libc] more precise spec for bzero · e38dd468
      Andre Maroneze authored
      e38dd468
    • Loïc Correnson's avatar
      [wp] cleaning · ccf0135f
      Loïc Correnson authored
      ccf0135f
    • Loïc Correnson's avatar
      Merge branch 'feature/nupw/updates-argon' into 'master' · ec3725b2
      Loïc Correnson authored 
      Backport of NUPW into master

See merge request frama-c/frama-c!2108
      ec3725b2
    • Loïc Correnson's avatar
      [wp] fix changelog · da6582bc
      Loïc Correnson authored
      da6582bc
    • Loïc Correnson's avatar
      Merge branch 'master' into feature/nupw/updates-argon · 71b49c6c
      Loïc Correnson authored 
      # Conflicts:
#	src/kernel_services/ast_data/property.ml
#	src/kernel_services/ast_data/property.mli
#	src/libraries/utils/sanitizer.ml
#	src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
#	src/plugins/wp/tests/wp/sharing.c.0.report.json
#	src/plugins/wp/tests/wp/wp_behav.c.0.report.json
#	src/plugins/wp/tests/wp/wp_call_pre.c.0.report.json
#	src/plugins/wp/tests/wp/wp_eqb.i.0.report.json
#	src/plugins/wp/tests/wp/wp_strategy.c.0.report.json
#	src/plugins/wp/tests/wp_acsl/assigns_path.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/assigns_range.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/cnf.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/div_mod.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/e_imply.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/equal.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json
#	src/plugins/wp/tests/wp_acsl/init_value_mem.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/logic.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/looplabels.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
#	src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
#	src/plugins/wp/tests/wp_acsl/range.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/reads.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/record.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/simpl_is_type.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/struct_use_case.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/unit_bit_test.c.0.report.json
#	src/plugins/wp/tests/wp_bts/bts0843.i.0.report.json
#	src/plugins/wp/tests/wp_bts/bts788.i.0.report.json
#	src/plugins/wp/tests/wp_bts/bts_1601.c.0.report.json
#	src/plugins/wp/tests/wp_bts/bts_2159.i.0.report.json
#	src/plugins/wp/tests/wp_bts/issue_508.c.0.report.json
#	src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i.0.report.json
#	src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
#	src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
#	src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
#	src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c.0.report.json
#	src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
#	src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
#	src/plugins/wp/tests/wp_hoare/byref.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/byref.i.1.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var2.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var2.i.1.report.json
#	src/plugins/wp/tests/wp_hoare/logicref.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/logicref_simple.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
#	src/plugins/wp/tests/wp_hoare/reference.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/reference_and_struct.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/reference_array.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/refguards.i.0.report.json
#	src/plugins/wp/tests/wp_manual/manual.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/bool.i.1.report.json
#	src/plugins/wp/tests/wp_plugin/copy.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/init_const_guard.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/initarr.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/injector.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
#	src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
#	src/plugins/wp/tests/wp_plugin/overassign.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/prenex.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/repeat.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/sequence.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/stmt.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/struct_hack.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/subset.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/trig.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/unsupported_init.i.0.report.json
#	src/plugins/wp/tests/wp_store/struct.i.0.report.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
#	src/plugins/wp/tests/wp_typed/array_initialized.c.1.report.json
#	src/plugins/wp/tests/wp_typed/avar.i.0.report.json
#	src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
#	src/plugins/wp/tests/wp_typed/struct_array_type.i.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_bitwise.c.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_local.c.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_local.c.1.report.json
#	src/plugins/wp/tests/wp_typed/unit_tset.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_bitwise.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_collect.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_init.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_swap.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_swap.i.1.report.json
#	src/plugins/wp/tests/wp_usage/caveat2.i.0.report.json
#	src/plugins/wp/tests/wp_usage/caveat_range.i.0.report.json
#	src/plugins/wp/tests/wp_usage/issue-189-bis.i.0.report.json
#	src/plugins/wp/tests/wp_usage/issue-189-bis.i.1.report.json
      71b49c6c
    • Virgile Prevosto's avatar
      Merge branch 'fix/andre/jcdb-verbosity' into 'master' · a3c3b7e3
      Virgile Prevosto authored 
      [Kernel] minimize verbosity of -json-compilation-database warnings

See merge request frama-c/frama-c!2117
      a3c3b7e3
    • Loïc Correnson's avatar
      [wp] fix C/ACSL literals · e8a5abf6
      Loïc Correnson authored
      e8a5abf6
    • Loïc Correnson's avatar
      Merge branch 'feature/property-names' into 'master' · 5f956e2e
      Loïc Correnson authored 
      [kernel] Refactored Property Names

Closes #12

See merge request frama-c/frama-c!2110
      5f956e2e
  5. Jan 31, 2019
  7. Jan 30, 2019
  9. Jan 29, 2019
  11. Jan 28, 2019
  13. Jan 25, 2019