0001103: Default @requires property for the [main] function - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0001103

Frama-C

Kernel

public

2012-02-22 09:52

2014-07-11 12:50

Reporter

Anne

Assigned To

virgile

Priority

normal

Severity

feature

Reproducibility

have not tried

Status

assigned

Resolution

open

Platform

OS

OS Version

Product Version

Target Version

Fixed in Version

Summary

0001103: Default @requires property for the [main] function

Description

I think that it would be great to generate a default @requires property for the 'main' function, wouldn't it ?

Additional Information

The one from [tests/aorai/test_recursion1.c] for instance seems ok.

Tags

No tags attached.

Relationships

related to

closed

Command line arguments (argc/argv) are not marked as valid

Notes
(0002722) virgile (developer) 2012-02-23 10:40	I guess that you mean that the main function should have as requires the fact that globals are initialized to 0 (provided we're not in -lib-entry mode)?

(0002723) Anne (reporter) 2012-02-23 12:07	No, not exactly. As I said, it is more about argc and argv like in the file [tests/aorai/test_recursion1.c] for instance.

Issue History
Date Modified	Username	Field	Change
2012-02-22 09:52	Anne	New Issue
2012-02-22 15:11	signoles	Status	new => assigned
2012-02-22 15:11	signoles	Assigned To	=> virgile
2012-02-23 10:40	virgile	Note Added: 0002722
2012-02-23 12:07	Anne	Note Added: 0002723
2014-07-11 12:27	yakobowski	Relationship added	related to 0001831

Copyright © 2000 - 2020 MantisBT Team