Frama-C
  • Features
  • Documentation
  • Publications
  • Blog
  • Jobs
  • Contact
  • Download

Blog

Back

Tag Archives: undefined-behavior

On the redundancy of C99's restrict
Pascal Cuoq on 25 July 2012

The restrict keyword in C99 C99 introduced a restrict keyword. The intention is to let the programmer specify the absence of alias between some inputs of a function ey is writing. Consider the function: int f1(int * restrict p int * restrict q) { *p = 1; *q = 2;...

Read More
« Previous 1 ... 2 3

Tags

undefined-behavior skein value ACSL Jessie derived-analysis unspecified-behavior CIL OCaml floating-point rant memcpy value-builtins conversions-and-promotions icpc2011 csmith position donut facetious-colleagues slicing CompCert big-round-numbers trail nitrogen link benchmarks rte obviously-terminates cybersecurity linking type-checking developer visitor restrict rers2012 cfg WP c11 c99 anonymous-arrays zlib metrics collaboration FLT_EVAL_METHOD function-pointers c-reduce Eva gui tutorial open-source-case-studies scripts usability windows-cygwin-wsl docker github ci test Ivette GUI event machdep parsing formal spec, ACSL, MetAcsl, RPP, Aoraï, Typestates
Copyright © 2007-2025 Frama-C. All Rights Reserved.
  • Terms Of Use
  • Authors
  • Acknowledgements