0002432: Attributes of size 1 are rejected - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002432

Frama-C

Kernel

public

2019-03-20 17:27

2019-04-09 17:28

Reporter

Stevendeo

Assigned To

virgile

Priority

low

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

OS Version

Product Version

Frama-C 18-Argon

Target Version

Fixed in Version

Frama-C 19-Potassium

Summary

0002432: Attributes of size 1 are rejected

Description

Attributes are parsed by Extlib.strip_underscore that removes underscores before and after a string. However, the function always returns an empty string when the size of the input is 1. The attribute is then rejected.
The error is not raised in Chlorine.

Steps To Reproduce

frama-c foo.c

Additional Information

Here is a possible bug fix

let strip_underscore s =
  let l = String.length s in
  if l = 1
  then
    match s with
      "_" -> ""
    | _ -> s
  else
    let rec start i =
      if i >= l then l-1
      else if s.[i] = '_' then start (i + 1) else i
    in
    let st = start 0 in
    if st = l - 1 then ""
    else begin
      let rec finish i =
        (* We know that we will stop at >= st >= 0 *)
        if s.[i] = '_' then finish (i - 1) else i
      in
      let fin = finish (l - 1) in
      String.sub s st (fin - st + 1)
    end

Tags

No tags attached.

Attached Files

foo.c [^] (52 bytes) 2019-03-20 17:27 [Show Content] [Hide Content]

int main(){
  int __attribute((t)) x;
  return 0;
}

Relationships

Notes
(0006762) virgile (developer) 2019-04-09 17:27	Actually, the main issue is returning l-1 when no non-underscore character is found. It should return l (and the test for emptiness be updated accordingly). This is fixed in dev branch and will appear in the next Frama-C release. Thanks for the report.

Issue History
Date Modified	Username	Field	Change
2019-03-20 17:27	Stevendeo	New Issue
2019-03-20 17:27	Stevendeo	File Added: foo.c
2019-04-09 17:27	virgile	Note Added: 0006762
2019-04-09 17:28	virgile	Status	new => resolved
2019-04-09 17:28	virgile	Fixed in Version	=> Frama-C 19-Potassium
2019-04-09 17:28	virgile	Resolution	open => fixed
2019-04-09 17:28	virgile	Assigned To	=> virgile