Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #135

Closed
Open
Created Aug 19, 2019 by mantis-gitlab-migration@mantis-gitlab-migration

E-ACSL: segmentation fault on a simple strlen function

ID0002472: This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002472 Frama-C Plug-in > E-ACSL public 2019-08-19 2019-08-22
Reporter evdenis Assigned To signoles Resolution no change required
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C 19-Potassium Target Version - Fixed in Version -

Description :

E-ACSL successfully generates executable for this example and fails at runtime with segmentation fault error in shadow_alloca function at initialization stage.

#include 
#include 
#include 

/*@ requires \exists size_t i; s[i] == '\0' && \valid_read(s+(0..i));
    assigns \nothing;
    ensures s[\result] == '\0';
    ensures \forall size_t j; 0 <= j < \result ==> s[j] != '\0';
 */
size_t strlen(char *s)
{
	size_t len;

	/*@ loop invariant \forall size_t i; i < len ==> s[i] != '\0';
	    loop assigns len;
	    loop variant SIZE_MAX - len;
	 */
	for(len = 0; s[len] != '\0'; ++len);

	return len;
}

int main(int argc, char *argv[])
{
	for(int i = 0; i < argc; ++i) {
		printf("%s: %d\n", argv[i], strlen(argv[i]));
	}
	return 0;
}

Additional Information :

$ gdb ./a.out.e-acsl Temporary breakpoint 1, main (argc=1, argv=0x7fffffffd3e8) at a.out.frama.c:278 278 __e_acsl_memory_init(& argc,& argv,8UL); Program received signal SIGSEGV, Segmentation fault. shadow_alloca (ptr=ptr@entry=0x7fffffffd298, size=size@entry=8) at /home/work/.opam/framac/bin/../share/frama-c/e-acsl//segment_model/e_acsl_segment_tracking.h:562 562 prim_shadow[i] = (code << 2);

main function could be simple. For example, fails also in this case: int main(void) { char *str = "0123456789"; printf("%s: %d\n", str, strlen(str)); return 0; }

Steps To Reproduce :

$ e-acsl-gcc.sh -c ./strlen.c $ ./a.out.e-acsl [1] 26340 segmentation fault (core dumped) ./a.out.e-acsl

Attachments

  • strlen.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking